0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 187 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 45 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 473 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇔, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇔, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
↳30 PiDP
↳31 UsableRulesProof (⇔, 0 ms)
↳32 PiDP
↳33 PiDPToQDPProof (⇒, 0 ms)
↳34 QDP
↳35 QDPSizeChangeProof (⇔, 0 ms)
↳36 YES
↳37 PiDP
↳38 UsableRulesProof (⇔, 0 ms)
↳39 PiDP
↳40 PiDPToQDPProof (⇒, 0 ms)
↳41 QDP
↳42 QDPSizeChangeProof (⇔, 0 ms)
↳43 YES
↳44 PiDP
↳45 UsableRulesProof (⇔, 0 ms)
↳46 PiDP
↳47 PiDPToQDPProof (⇒, 17 ms)
↳48 QDP
↳49 QDPSizeChangeProof (⇔, 0 ms)
↳50 YES
↳51 PiDP
↳52 UsableRulesProof (⇔, 0 ms)
↳53 PiDP
↳54 PiDPToQDPProof (⇒, 0 ms)
↳55 QDP
↳56 QDPSizeChangeProof (⇔, 0 ms)
↳57 YES
inG_in_ag(T6, tree(T6, T7, T8)) → inG_out_ag(T6, tree(T6, T7, T8))
inG_in_ag(0, tree(s(T22), T15, T16)) → U11_ag(T22, T15, T16, inA_in_g(T15))
inA_in_g(tree(0, T35, T36)) → inA_out_g(tree(0, T35, T36))
inA_in_g(tree(T49, T50, T51)) → U1_g(T49, T50, T51, lessB_in_g(T49))
lessB_in_g(s(T60)) → lessB_out_g(s(T60))
U1_g(T49, T50, T51, lessB_out_g(T49)) → inA_out_g(tree(T49, T50, T51))
U1_g(T49, T50, T51, lessB_out_g(T49)) → U2_g(T49, T50, T51, inA_in_g(T50))
U2_g(T49, T50, T51, inA_out_g(T50)) → inA_out_g(tree(T49, T50, T51))
U11_ag(T22, T15, T16, inA_out_g(T15)) → inG_out_ag(0, tree(s(T22), T15, T16))
inG_in_ag(s(T89), tree(s(T88), T15, T16)) → U12_ag(T89, T88, T15, T16, pF_in_agg(T89, T88, T15))
pF_in_agg(T89, T88, T15) → U5_agg(T89, T88, T15, lessD_in_ag(T89, T88))
lessD_in_ag(0, s(T99)) → lessD_out_ag(0, s(T99))
lessD_in_ag(s(T106), s(T105)) → U3_ag(T106, T105, lessD_in_ag(T106, T105))
U3_ag(T106, T105, lessD_out_ag(T106, T105)) → lessD_out_ag(s(T106), s(T105))
U5_agg(T89, T88, T15, lessD_out_ag(T89, T88)) → pF_out_agg(T89, T88, T15)
pF_in_agg(T92, T88, T15) → U6_agg(T92, T88, T15, lessD_in_ag(T92, T88))
U6_agg(T92, T88, T15, lessD_out_ag(T92, T88)) → U7_agg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T6, tree(T6, T7, T8)) → inG_out_gg(T6, tree(T6, T7, T8))
inG_in_gg(0, tree(s(T22), T15, T16)) → U11_gg(T22, T15, T16, inA_in_g(T15))
U11_gg(T22, T15, T16, inA_out_g(T15)) → inG_out_gg(0, tree(s(T22), T15, T16))
inG_in_gg(s(T89), tree(s(T88), T15, T16)) → U12_gg(T89, T88, T15, T16, pF_in_ggg(T89, T88, T15))
pF_in_ggg(T89, T88, T15) → U5_ggg(T89, T88, T15, lessD_in_gg(T89, T88))
lessD_in_gg(0, s(T99)) → lessD_out_gg(0, s(T99))
lessD_in_gg(s(T106), s(T105)) → U3_gg(T106, T105, lessD_in_gg(T106, T105))
U3_gg(T106, T105, lessD_out_gg(T106, T105)) → lessD_out_gg(s(T106), s(T105))
U5_ggg(T89, T88, T15, lessD_out_gg(T89, T88)) → pF_out_ggg(T89, T88, T15)
pF_in_ggg(T92, T88, T15) → U6_ggg(T92, T88, T15, lessD_in_gg(T92, T88))
U6_ggg(T92, T88, T15, lessD_out_gg(T92, T88)) → U7_ggg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T130, tree(T127, T128, T129)) → U13_gg(T130, T127, T128, T129, pH_in_ggg(T127, T130, T129))
pH_in_ggg(T127, T130, T129) → U8_ggg(T127, T130, T129, lessE_in_gg(T127, T130))
lessE_in_gg(0, s(T140)) → lessE_out_gg(0, s(T140))
lessE_in_gg(s(T145), s(T147)) → U4_gg(T145, T147, lessE_in_gg(T145, T147))
U4_gg(T145, T147, lessE_out_gg(T145, T147)) → lessE_out_gg(s(T145), s(T147))
U8_ggg(T127, T130, T129, lessE_out_gg(T127, T130)) → pH_out_ggg(T127, T130, T129)
pH_in_ggg(T127, T133, T129) → U9_ggg(T127, T133, T129, lessE_in_gg(T127, T133))
U9_ggg(T127, T133, T129, lessE_out_gg(T127, T133)) → U10_ggg(T127, T133, T129, inG_in_gg(T133, T129))
inG_in_gg(0, tree(s(T169), T162, T163)) → U14_gg(T169, T162, T163, inA_in_g(T162))
U14_gg(T169, T162, T163, inA_out_g(T162)) → inG_out_gg(0, tree(s(T169), T162, T163))
inG_in_gg(s(T184), tree(s(T183), T162, T163)) → U15_gg(T184, T183, T162, T163, pF_in_ggg(T184, T183, T162))
U15_gg(T184, T183, T162, T163, pF_out_ggg(T184, T183, T162)) → inG_out_gg(s(T184), tree(s(T183), T162, T163))
inG_in_gg(T202, tree(T199, T200, T201)) → U16_gg(T202, T199, T200, T201, pH_in_ggg(T199, T202, T201))
U16_gg(T202, T199, T200, T201, pH_out_ggg(T199, T202, T201)) → inG_out_gg(T202, tree(T199, T200, T201))
inG_in_gg(s(T219), tree(0, T211, T212)) → U17_gg(T219, T211, T212, inG_in_gg(s(T219), T212))
inG_in_gg(s(T232), tree(s(T230), T211, T212)) → U18_gg(T232, T230, T211, T212, lessE_in_gg(T230, T232))
U18_gg(T232, T230, T211, T212, lessE_out_gg(T230, T232)) → inG_out_gg(s(T232), tree(s(T230), T211, T212))
inG_in_gg(s(T235), tree(s(T230), T211, T212)) → U19_gg(T235, T230, T211, T212, lessE_in_gg(T230, T235))
U19_gg(T235, T230, T211, T212, lessE_out_gg(T230, T235)) → U20_gg(T235, T230, T211, T212, inG_in_gg(s(T235), T212))
U20_gg(T235, T230, T211, T212, inG_out_gg(s(T235), T212)) → inG_out_gg(s(T235), tree(s(T230), T211, T212))
U17_gg(T219, T211, T212, inG_out_gg(s(T219), T212)) → inG_out_gg(s(T219), tree(0, T211, T212))
U10_ggg(T127, T133, T129, inG_out_gg(T133, T129)) → pH_out_ggg(T127, T133, T129)
U13_gg(T130, T127, T128, T129, pH_out_ggg(T127, T130, T129)) → inG_out_gg(T130, tree(T127, T128, T129))
U7_ggg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_ggg(T92, T88, T15)
U12_gg(T89, T88, T15, T16, pF_out_ggg(T89, T88, T15)) → inG_out_gg(s(T89), tree(s(T88), T15, T16))
U7_agg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_agg(T92, T88, T15)
U12_ag(T89, T88, T15, T16, pF_out_agg(T89, T88, T15)) → inG_out_ag(s(T89), tree(s(T88), T15, T16))
inG_in_ag(T130, tree(T127, T128, T129)) → U13_ag(T130, T127, T128, T129, pH_in_gag(T127, T130, T129))
pH_in_gag(T127, T130, T129) → U8_gag(T127, T130, T129, lessE_in_ga(T127, T130))
lessE_in_ga(0, s(T140)) → lessE_out_ga(0, s(T140))
lessE_in_ga(s(T145), s(T147)) → U4_ga(T145, T147, lessE_in_ga(T145, T147))
U4_ga(T145, T147, lessE_out_ga(T145, T147)) → lessE_out_ga(s(T145), s(T147))
U8_gag(T127, T130, T129, lessE_out_ga(T127, T130)) → pH_out_gag(T127, T130, T129)
pH_in_gag(T127, T133, T129) → U9_gag(T127, T133, T129, lessE_in_ga(T127, T133))
U9_gag(T127, T133, T129, lessE_out_ga(T127, T133)) → U10_gag(T127, T133, T129, inG_in_ag(T133, T129))
inG_in_ag(0, tree(s(T169), T162, T163)) → U14_ag(T169, T162, T163, inA_in_g(T162))
U14_ag(T169, T162, T163, inA_out_g(T162)) → inG_out_ag(0, tree(s(T169), T162, T163))
inG_in_ag(s(T184), tree(s(T183), T162, T163)) → U15_ag(T184, T183, T162, T163, pF_in_agg(T184, T183, T162))
U15_ag(T184, T183, T162, T163, pF_out_agg(T184, T183, T162)) → inG_out_ag(s(T184), tree(s(T183), T162, T163))
inG_in_ag(T202, tree(T199, T200, T201)) → U16_ag(T202, T199, T200, T201, pH_in_gag(T199, T202, T201))
U16_ag(T202, T199, T200, T201, pH_out_gag(T199, T202, T201)) → inG_out_ag(T202, tree(T199, T200, T201))
inG_in_ag(s(T219), tree(0, T211, T212)) → U17_ag(T219, T211, T212, inG_in_ag(s(T219), T212))
inG_in_ag(s(T232), tree(s(T230), T211, T212)) → U18_ag(T232, T230, T211, T212, lessE_in_ga(T230, T232))
U18_ag(T232, T230, T211, T212, lessE_out_ga(T230, T232)) → inG_out_ag(s(T232), tree(s(T230), T211, T212))
inG_in_ag(s(T235), tree(s(T230), T211, T212)) → U19_ag(T235, T230, T211, T212, lessE_in_ga(T230, T235))
U19_ag(T235, T230, T211, T212, lessE_out_ga(T230, T235)) → U20_ag(T235, T230, T211, T212, inG_in_ag(s(T235), T212))
U20_ag(T235, T230, T211, T212, inG_out_ag(s(T235), T212)) → inG_out_ag(s(T235), tree(s(T230), T211, T212))
U17_ag(T219, T211, T212, inG_out_ag(s(T219), T212)) → inG_out_ag(s(T219), tree(0, T211, T212))
U10_gag(T127, T133, T129, inG_out_ag(T133, T129)) → pH_out_gag(T127, T133, T129)
U13_ag(T130, T127, T128, T129, pH_out_gag(T127, T130, T129)) → inG_out_ag(T130, tree(T127, T128, T129))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
inG_in_ag(T6, tree(T6, T7, T8)) → inG_out_ag(T6, tree(T6, T7, T8))
inG_in_ag(0, tree(s(T22), T15, T16)) → U11_ag(T22, T15, T16, inA_in_g(T15))
inA_in_g(tree(0, T35, T36)) → inA_out_g(tree(0, T35, T36))
inA_in_g(tree(T49, T50, T51)) → U1_g(T49, T50, T51, lessB_in_g(T49))
lessB_in_g(s(T60)) → lessB_out_g(s(T60))
U1_g(T49, T50, T51, lessB_out_g(T49)) → inA_out_g(tree(T49, T50, T51))
U1_g(T49, T50, T51, lessB_out_g(T49)) → U2_g(T49, T50, T51, inA_in_g(T50))
U2_g(T49, T50, T51, inA_out_g(T50)) → inA_out_g(tree(T49, T50, T51))
U11_ag(T22, T15, T16, inA_out_g(T15)) → inG_out_ag(0, tree(s(T22), T15, T16))
inG_in_ag(s(T89), tree(s(T88), T15, T16)) → U12_ag(T89, T88, T15, T16, pF_in_agg(T89, T88, T15))
pF_in_agg(T89, T88, T15) → U5_agg(T89, T88, T15, lessD_in_ag(T89, T88))
lessD_in_ag(0, s(T99)) → lessD_out_ag(0, s(T99))
lessD_in_ag(s(T106), s(T105)) → U3_ag(T106, T105, lessD_in_ag(T106, T105))
U3_ag(T106, T105, lessD_out_ag(T106, T105)) → lessD_out_ag(s(T106), s(T105))
U5_agg(T89, T88, T15, lessD_out_ag(T89, T88)) → pF_out_agg(T89, T88, T15)
pF_in_agg(T92, T88, T15) → U6_agg(T92, T88, T15, lessD_in_ag(T92, T88))
U6_agg(T92, T88, T15, lessD_out_ag(T92, T88)) → U7_agg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T6, tree(T6, T7, T8)) → inG_out_gg(T6, tree(T6, T7, T8))
inG_in_gg(0, tree(s(T22), T15, T16)) → U11_gg(T22, T15, T16, inA_in_g(T15))
U11_gg(T22, T15, T16, inA_out_g(T15)) → inG_out_gg(0, tree(s(T22), T15, T16))
inG_in_gg(s(T89), tree(s(T88), T15, T16)) → U12_gg(T89, T88, T15, T16, pF_in_ggg(T89, T88, T15))
pF_in_ggg(T89, T88, T15) → U5_ggg(T89, T88, T15, lessD_in_gg(T89, T88))
lessD_in_gg(0, s(T99)) → lessD_out_gg(0, s(T99))
lessD_in_gg(s(T106), s(T105)) → U3_gg(T106, T105, lessD_in_gg(T106, T105))
U3_gg(T106, T105, lessD_out_gg(T106, T105)) → lessD_out_gg(s(T106), s(T105))
U5_ggg(T89, T88, T15, lessD_out_gg(T89, T88)) → pF_out_ggg(T89, T88, T15)
pF_in_ggg(T92, T88, T15) → U6_ggg(T92, T88, T15, lessD_in_gg(T92, T88))
U6_ggg(T92, T88, T15, lessD_out_gg(T92, T88)) → U7_ggg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T130, tree(T127, T128, T129)) → U13_gg(T130, T127, T128, T129, pH_in_ggg(T127, T130, T129))
pH_in_ggg(T127, T130, T129) → U8_ggg(T127, T130, T129, lessE_in_gg(T127, T130))
lessE_in_gg(0, s(T140)) → lessE_out_gg(0, s(T140))
lessE_in_gg(s(T145), s(T147)) → U4_gg(T145, T147, lessE_in_gg(T145, T147))
U4_gg(T145, T147, lessE_out_gg(T145, T147)) → lessE_out_gg(s(T145), s(T147))
U8_ggg(T127, T130, T129, lessE_out_gg(T127, T130)) → pH_out_ggg(T127, T130, T129)
pH_in_ggg(T127, T133, T129) → U9_ggg(T127, T133, T129, lessE_in_gg(T127, T133))
U9_ggg(T127, T133, T129, lessE_out_gg(T127, T133)) → U10_ggg(T127, T133, T129, inG_in_gg(T133, T129))
inG_in_gg(0, tree(s(T169), T162, T163)) → U14_gg(T169, T162, T163, inA_in_g(T162))
U14_gg(T169, T162, T163, inA_out_g(T162)) → inG_out_gg(0, tree(s(T169), T162, T163))
inG_in_gg(s(T184), tree(s(T183), T162, T163)) → U15_gg(T184, T183, T162, T163, pF_in_ggg(T184, T183, T162))
U15_gg(T184, T183, T162, T163, pF_out_ggg(T184, T183, T162)) → inG_out_gg(s(T184), tree(s(T183), T162, T163))
inG_in_gg(T202, tree(T199, T200, T201)) → U16_gg(T202, T199, T200, T201, pH_in_ggg(T199, T202, T201))
U16_gg(T202, T199, T200, T201, pH_out_ggg(T199, T202, T201)) → inG_out_gg(T202, tree(T199, T200, T201))
inG_in_gg(s(T219), tree(0, T211, T212)) → U17_gg(T219, T211, T212, inG_in_gg(s(T219), T212))
inG_in_gg(s(T232), tree(s(T230), T211, T212)) → U18_gg(T232, T230, T211, T212, lessE_in_gg(T230, T232))
U18_gg(T232, T230, T211, T212, lessE_out_gg(T230, T232)) → inG_out_gg(s(T232), tree(s(T230), T211, T212))
inG_in_gg(s(T235), tree(s(T230), T211, T212)) → U19_gg(T235, T230, T211, T212, lessE_in_gg(T230, T235))
U19_gg(T235, T230, T211, T212, lessE_out_gg(T230, T235)) → U20_gg(T235, T230, T211, T212, inG_in_gg(s(T235), T212))
U20_gg(T235, T230, T211, T212, inG_out_gg(s(T235), T212)) → inG_out_gg(s(T235), tree(s(T230), T211, T212))
U17_gg(T219, T211, T212, inG_out_gg(s(T219), T212)) → inG_out_gg(s(T219), tree(0, T211, T212))
U10_ggg(T127, T133, T129, inG_out_gg(T133, T129)) → pH_out_ggg(T127, T133, T129)
U13_gg(T130, T127, T128, T129, pH_out_ggg(T127, T130, T129)) → inG_out_gg(T130, tree(T127, T128, T129))
U7_ggg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_ggg(T92, T88, T15)
U12_gg(T89, T88, T15, T16, pF_out_ggg(T89, T88, T15)) → inG_out_gg(s(T89), tree(s(T88), T15, T16))
U7_agg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_agg(T92, T88, T15)
U12_ag(T89, T88, T15, T16, pF_out_agg(T89, T88, T15)) → inG_out_ag(s(T89), tree(s(T88), T15, T16))
inG_in_ag(T130, tree(T127, T128, T129)) → U13_ag(T130, T127, T128, T129, pH_in_gag(T127, T130, T129))
pH_in_gag(T127, T130, T129) → U8_gag(T127, T130, T129, lessE_in_ga(T127, T130))
lessE_in_ga(0, s(T140)) → lessE_out_ga(0, s(T140))
lessE_in_ga(s(T145), s(T147)) → U4_ga(T145, T147, lessE_in_ga(T145, T147))
U4_ga(T145, T147, lessE_out_ga(T145, T147)) → lessE_out_ga(s(T145), s(T147))
U8_gag(T127, T130, T129, lessE_out_ga(T127, T130)) → pH_out_gag(T127, T130, T129)
pH_in_gag(T127, T133, T129) → U9_gag(T127, T133, T129, lessE_in_ga(T127, T133))
U9_gag(T127, T133, T129, lessE_out_ga(T127, T133)) → U10_gag(T127, T133, T129, inG_in_ag(T133, T129))
inG_in_ag(0, tree(s(T169), T162, T163)) → U14_ag(T169, T162, T163, inA_in_g(T162))
U14_ag(T169, T162, T163, inA_out_g(T162)) → inG_out_ag(0, tree(s(T169), T162, T163))
inG_in_ag(s(T184), tree(s(T183), T162, T163)) → U15_ag(T184, T183, T162, T163, pF_in_agg(T184, T183, T162))
U15_ag(T184, T183, T162, T163, pF_out_agg(T184, T183, T162)) → inG_out_ag(s(T184), tree(s(T183), T162, T163))
inG_in_ag(T202, tree(T199, T200, T201)) → U16_ag(T202, T199, T200, T201, pH_in_gag(T199, T202, T201))
U16_ag(T202, T199, T200, T201, pH_out_gag(T199, T202, T201)) → inG_out_ag(T202, tree(T199, T200, T201))
inG_in_ag(s(T219), tree(0, T211, T212)) → U17_ag(T219, T211, T212, inG_in_ag(s(T219), T212))
inG_in_ag(s(T232), tree(s(T230), T211, T212)) → U18_ag(T232, T230, T211, T212, lessE_in_ga(T230, T232))
U18_ag(T232, T230, T211, T212, lessE_out_ga(T230, T232)) → inG_out_ag(s(T232), tree(s(T230), T211, T212))
inG_in_ag(s(T235), tree(s(T230), T211, T212)) → U19_ag(T235, T230, T211, T212, lessE_in_ga(T230, T235))
U19_ag(T235, T230, T211, T212, lessE_out_ga(T230, T235)) → U20_ag(T235, T230, T211, T212, inG_in_ag(s(T235), T212))
U20_ag(T235, T230, T211, T212, inG_out_ag(s(T235), T212)) → inG_out_ag(s(T235), tree(s(T230), T211, T212))
U17_ag(T219, T211, T212, inG_out_ag(s(T219), T212)) → inG_out_ag(s(T219), tree(0, T211, T212))
U10_gag(T127, T133, T129, inG_out_ag(T133, T129)) → pH_out_gag(T127, T133, T129)
U13_ag(T130, T127, T128, T129, pH_out_gag(T127, T130, T129)) → inG_out_ag(T130, tree(T127, T128, T129))
ING_IN_AG(0, tree(s(T22), T15, T16)) → U11_AG(T22, T15, T16, inA_in_g(T15))
ING_IN_AG(0, tree(s(T22), T15, T16)) → INA_IN_G(T15)
INA_IN_G(tree(T49, T50, T51)) → U1_G(T49, T50, T51, lessB_in_g(T49))
INA_IN_G(tree(T49, T50, T51)) → LESSB_IN_G(T49)
U1_G(T49, T50, T51, lessB_out_g(T49)) → U2_G(T49, T50, T51, inA_in_g(T50))
U1_G(T49, T50, T51, lessB_out_g(T49)) → INA_IN_G(T50)
ING_IN_AG(s(T89), tree(s(T88), T15, T16)) → U12_AG(T89, T88, T15, T16, pF_in_agg(T89, T88, T15))
ING_IN_AG(s(T89), tree(s(T88), T15, T16)) → PF_IN_AGG(T89, T88, T15)
PF_IN_AGG(T89, T88, T15) → U5_AGG(T89, T88, T15, lessD_in_ag(T89, T88))
PF_IN_AGG(T89, T88, T15) → LESSD_IN_AG(T89, T88)
LESSD_IN_AG(s(T106), s(T105)) → U3_AG(T106, T105, lessD_in_ag(T106, T105))
LESSD_IN_AG(s(T106), s(T105)) → LESSD_IN_AG(T106, T105)
PF_IN_AGG(T92, T88, T15) → U6_AGG(T92, T88, T15, lessD_in_ag(T92, T88))
U6_AGG(T92, T88, T15, lessD_out_ag(T92, T88)) → U7_AGG(T92, T88, T15, inG_in_gg(s(T92), T15))
U6_AGG(T92, T88, T15, lessD_out_ag(T92, T88)) → ING_IN_GG(s(T92), T15)
ING_IN_GG(0, tree(s(T22), T15, T16)) → U11_GG(T22, T15, T16, inA_in_g(T15))
ING_IN_GG(0, tree(s(T22), T15, T16)) → INA_IN_G(T15)
ING_IN_GG(s(T89), tree(s(T88), T15, T16)) → U12_GG(T89, T88, T15, T16, pF_in_ggg(T89, T88, T15))
ING_IN_GG(s(T89), tree(s(T88), T15, T16)) → PF_IN_GGG(T89, T88, T15)
PF_IN_GGG(T89, T88, T15) → U5_GGG(T89, T88, T15, lessD_in_gg(T89, T88))
PF_IN_GGG(T89, T88, T15) → LESSD_IN_GG(T89, T88)
LESSD_IN_GG(s(T106), s(T105)) → U3_GG(T106, T105, lessD_in_gg(T106, T105))
LESSD_IN_GG(s(T106), s(T105)) → LESSD_IN_GG(T106, T105)
PF_IN_GGG(T92, T88, T15) → U6_GGG(T92, T88, T15, lessD_in_gg(T92, T88))
U6_GGG(T92, T88, T15, lessD_out_gg(T92, T88)) → U7_GGG(T92, T88, T15, inG_in_gg(s(T92), T15))
U6_GGG(T92, T88, T15, lessD_out_gg(T92, T88)) → ING_IN_GG(s(T92), T15)
ING_IN_GG(T130, tree(T127, T128, T129)) → U13_GG(T130, T127, T128, T129, pH_in_ggg(T127, T130, T129))
ING_IN_GG(T130, tree(T127, T128, T129)) → PH_IN_GGG(T127, T130, T129)
PH_IN_GGG(T127, T130, T129) → U8_GGG(T127, T130, T129, lessE_in_gg(T127, T130))
PH_IN_GGG(T127, T130, T129) → LESSE_IN_GG(T127, T130)
LESSE_IN_GG(s(T145), s(T147)) → U4_GG(T145, T147, lessE_in_gg(T145, T147))
LESSE_IN_GG(s(T145), s(T147)) → LESSE_IN_GG(T145, T147)
PH_IN_GGG(T127, T133, T129) → U9_GGG(T127, T133, T129, lessE_in_gg(T127, T133))
U9_GGG(T127, T133, T129, lessE_out_gg(T127, T133)) → U10_GGG(T127, T133, T129, inG_in_gg(T133, T129))
U9_GGG(T127, T133, T129, lessE_out_gg(T127, T133)) → ING_IN_GG(T133, T129)
ING_IN_GG(0, tree(s(T169), T162, T163)) → U14_GG(T169, T162, T163, inA_in_g(T162))
ING_IN_GG(s(T184), tree(s(T183), T162, T163)) → U15_GG(T184, T183, T162, T163, pF_in_ggg(T184, T183, T162))
ING_IN_GG(T202, tree(T199, T200, T201)) → U16_GG(T202, T199, T200, T201, pH_in_ggg(T199, T202, T201))
ING_IN_GG(s(T219), tree(0, T211, T212)) → U17_GG(T219, T211, T212, inG_in_gg(s(T219), T212))
ING_IN_GG(s(T219), tree(0, T211, T212)) → ING_IN_GG(s(T219), T212)
ING_IN_GG(s(T232), tree(s(T230), T211, T212)) → U18_GG(T232, T230, T211, T212, lessE_in_gg(T230, T232))
ING_IN_GG(s(T232), tree(s(T230), T211, T212)) → LESSE_IN_GG(T230, T232)
ING_IN_GG(s(T235), tree(s(T230), T211, T212)) → U19_GG(T235, T230, T211, T212, lessE_in_gg(T230, T235))
U19_GG(T235, T230, T211, T212, lessE_out_gg(T230, T235)) → U20_GG(T235, T230, T211, T212, inG_in_gg(s(T235), T212))
U19_GG(T235, T230, T211, T212, lessE_out_gg(T230, T235)) → ING_IN_GG(s(T235), T212)
ING_IN_AG(T130, tree(T127, T128, T129)) → U13_AG(T130, T127, T128, T129, pH_in_gag(T127, T130, T129))
ING_IN_AG(T130, tree(T127, T128, T129)) → PH_IN_GAG(T127, T130, T129)
PH_IN_GAG(T127, T130, T129) → U8_GAG(T127, T130, T129, lessE_in_ga(T127, T130))
PH_IN_GAG(T127, T130, T129) → LESSE_IN_GA(T127, T130)
LESSE_IN_GA(s(T145), s(T147)) → U4_GA(T145, T147, lessE_in_ga(T145, T147))
LESSE_IN_GA(s(T145), s(T147)) → LESSE_IN_GA(T145, T147)
PH_IN_GAG(T127, T133, T129) → U9_GAG(T127, T133, T129, lessE_in_ga(T127, T133))
U9_GAG(T127, T133, T129, lessE_out_ga(T127, T133)) → U10_GAG(T127, T133, T129, inG_in_ag(T133, T129))
U9_GAG(T127, T133, T129, lessE_out_ga(T127, T133)) → ING_IN_AG(T133, T129)
ING_IN_AG(0, tree(s(T169), T162, T163)) → U14_AG(T169, T162, T163, inA_in_g(T162))
ING_IN_AG(s(T184), tree(s(T183), T162, T163)) → U15_AG(T184, T183, T162, T163, pF_in_agg(T184, T183, T162))
ING_IN_AG(T202, tree(T199, T200, T201)) → U16_AG(T202, T199, T200, T201, pH_in_gag(T199, T202, T201))
ING_IN_AG(s(T219), tree(0, T211, T212)) → U17_AG(T219, T211, T212, inG_in_ag(s(T219), T212))
ING_IN_AG(s(T219), tree(0, T211, T212)) → ING_IN_AG(s(T219), T212)
ING_IN_AG(s(T232), tree(s(T230), T211, T212)) → U18_AG(T232, T230, T211, T212, lessE_in_ga(T230, T232))
ING_IN_AG(s(T232), tree(s(T230), T211, T212)) → LESSE_IN_GA(T230, T232)
ING_IN_AG(s(T235), tree(s(T230), T211, T212)) → U19_AG(T235, T230, T211, T212, lessE_in_ga(T230, T235))
U19_AG(T235, T230, T211, T212, lessE_out_ga(T230, T235)) → U20_AG(T235, T230, T211, T212, inG_in_ag(s(T235), T212))
U19_AG(T235, T230, T211, T212, lessE_out_ga(T230, T235)) → ING_IN_AG(s(T235), T212)
inG_in_ag(T6, tree(T6, T7, T8)) → inG_out_ag(T6, tree(T6, T7, T8))
inG_in_ag(0, tree(s(T22), T15, T16)) → U11_ag(T22, T15, T16, inA_in_g(T15))
inA_in_g(tree(0, T35, T36)) → inA_out_g(tree(0, T35, T36))
inA_in_g(tree(T49, T50, T51)) → U1_g(T49, T50, T51, lessB_in_g(T49))
lessB_in_g(s(T60)) → lessB_out_g(s(T60))
U1_g(T49, T50, T51, lessB_out_g(T49)) → inA_out_g(tree(T49, T50, T51))
U1_g(T49, T50, T51, lessB_out_g(T49)) → U2_g(T49, T50, T51, inA_in_g(T50))
U2_g(T49, T50, T51, inA_out_g(T50)) → inA_out_g(tree(T49, T50, T51))
U11_ag(T22, T15, T16, inA_out_g(T15)) → inG_out_ag(0, tree(s(T22), T15, T16))
inG_in_ag(s(T89), tree(s(T88), T15, T16)) → U12_ag(T89, T88, T15, T16, pF_in_agg(T89, T88, T15))
pF_in_agg(T89, T88, T15) → U5_agg(T89, T88, T15, lessD_in_ag(T89, T88))
lessD_in_ag(0, s(T99)) → lessD_out_ag(0, s(T99))
lessD_in_ag(s(T106), s(T105)) → U3_ag(T106, T105, lessD_in_ag(T106, T105))
U3_ag(T106, T105, lessD_out_ag(T106, T105)) → lessD_out_ag(s(T106), s(T105))
U5_agg(T89, T88, T15, lessD_out_ag(T89, T88)) → pF_out_agg(T89, T88, T15)
pF_in_agg(T92, T88, T15) → U6_agg(T92, T88, T15, lessD_in_ag(T92, T88))
U6_agg(T92, T88, T15, lessD_out_ag(T92, T88)) → U7_agg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T6, tree(T6, T7, T8)) → inG_out_gg(T6, tree(T6, T7, T8))
inG_in_gg(0, tree(s(T22), T15, T16)) → U11_gg(T22, T15, T16, inA_in_g(T15))
U11_gg(T22, T15, T16, inA_out_g(T15)) → inG_out_gg(0, tree(s(T22), T15, T16))
inG_in_gg(s(T89), tree(s(T88), T15, T16)) → U12_gg(T89, T88, T15, T16, pF_in_ggg(T89, T88, T15))
pF_in_ggg(T89, T88, T15) → U5_ggg(T89, T88, T15, lessD_in_gg(T89, T88))
lessD_in_gg(0, s(T99)) → lessD_out_gg(0, s(T99))
lessD_in_gg(s(T106), s(T105)) → U3_gg(T106, T105, lessD_in_gg(T106, T105))
U3_gg(T106, T105, lessD_out_gg(T106, T105)) → lessD_out_gg(s(T106), s(T105))
U5_ggg(T89, T88, T15, lessD_out_gg(T89, T88)) → pF_out_ggg(T89, T88, T15)
pF_in_ggg(T92, T88, T15) → U6_ggg(T92, T88, T15, lessD_in_gg(T92, T88))
U6_ggg(T92, T88, T15, lessD_out_gg(T92, T88)) → U7_ggg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T130, tree(T127, T128, T129)) → U13_gg(T130, T127, T128, T129, pH_in_ggg(T127, T130, T129))
pH_in_ggg(T127, T130, T129) → U8_ggg(T127, T130, T129, lessE_in_gg(T127, T130))
lessE_in_gg(0, s(T140)) → lessE_out_gg(0, s(T140))
lessE_in_gg(s(T145), s(T147)) → U4_gg(T145, T147, lessE_in_gg(T145, T147))
U4_gg(T145, T147, lessE_out_gg(T145, T147)) → lessE_out_gg(s(T145), s(T147))
U8_ggg(T127, T130, T129, lessE_out_gg(T127, T130)) → pH_out_ggg(T127, T130, T129)
pH_in_ggg(T127, T133, T129) → U9_ggg(T127, T133, T129, lessE_in_gg(T127, T133))
U9_ggg(T127, T133, T129, lessE_out_gg(T127, T133)) → U10_ggg(T127, T133, T129, inG_in_gg(T133, T129))
inG_in_gg(0, tree(s(T169), T162, T163)) → U14_gg(T169, T162, T163, inA_in_g(T162))
U14_gg(T169, T162, T163, inA_out_g(T162)) → inG_out_gg(0, tree(s(T169), T162, T163))
inG_in_gg(s(T184), tree(s(T183), T162, T163)) → U15_gg(T184, T183, T162, T163, pF_in_ggg(T184, T183, T162))
U15_gg(T184, T183, T162, T163, pF_out_ggg(T184, T183, T162)) → inG_out_gg(s(T184), tree(s(T183), T162, T163))
inG_in_gg(T202, tree(T199, T200, T201)) → U16_gg(T202, T199, T200, T201, pH_in_ggg(T199, T202, T201))
U16_gg(T202, T199, T200, T201, pH_out_ggg(T199, T202, T201)) → inG_out_gg(T202, tree(T199, T200, T201))
inG_in_gg(s(T219), tree(0, T211, T212)) → U17_gg(T219, T211, T212, inG_in_gg(s(T219), T212))
inG_in_gg(s(T232), tree(s(T230), T211, T212)) → U18_gg(T232, T230, T211, T212, lessE_in_gg(T230, T232))
U18_gg(T232, T230, T211, T212, lessE_out_gg(T230, T232)) → inG_out_gg(s(T232), tree(s(T230), T211, T212))
inG_in_gg(s(T235), tree(s(T230), T211, T212)) → U19_gg(T235, T230, T211, T212, lessE_in_gg(T230, T235))
U19_gg(T235, T230, T211, T212, lessE_out_gg(T230, T235)) → U20_gg(T235, T230, T211, T212, inG_in_gg(s(T235), T212))
U20_gg(T235, T230, T211, T212, inG_out_gg(s(T235), T212)) → inG_out_gg(s(T235), tree(s(T230), T211, T212))
U17_gg(T219, T211, T212, inG_out_gg(s(T219), T212)) → inG_out_gg(s(T219), tree(0, T211, T212))
U10_ggg(T127, T133, T129, inG_out_gg(T133, T129)) → pH_out_ggg(T127, T133, T129)
U13_gg(T130, T127, T128, T129, pH_out_ggg(T127, T130, T129)) → inG_out_gg(T130, tree(T127, T128, T129))
U7_ggg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_ggg(T92, T88, T15)
U12_gg(T89, T88, T15, T16, pF_out_ggg(T89, T88, T15)) → inG_out_gg(s(T89), tree(s(T88), T15, T16))
U7_agg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_agg(T92, T88, T15)
U12_ag(T89, T88, T15, T16, pF_out_agg(T89, T88, T15)) → inG_out_ag(s(T89), tree(s(T88), T15, T16))
inG_in_ag(T130, tree(T127, T128, T129)) → U13_ag(T130, T127, T128, T129, pH_in_gag(T127, T130, T129))
pH_in_gag(T127, T130, T129) → U8_gag(T127, T130, T129, lessE_in_ga(T127, T130))
lessE_in_ga(0, s(T140)) → lessE_out_ga(0, s(T140))
lessE_in_ga(s(T145), s(T147)) → U4_ga(T145, T147, lessE_in_ga(T145, T147))
U4_ga(T145, T147, lessE_out_ga(T145, T147)) → lessE_out_ga(s(T145), s(T147))
U8_gag(T127, T130, T129, lessE_out_ga(T127, T130)) → pH_out_gag(T127, T130, T129)
pH_in_gag(T127, T133, T129) → U9_gag(T127, T133, T129, lessE_in_ga(T127, T133))
U9_gag(T127, T133, T129, lessE_out_ga(T127, T133)) → U10_gag(T127, T133, T129, inG_in_ag(T133, T129))
inG_in_ag(0, tree(s(T169), T162, T163)) → U14_ag(T169, T162, T163, inA_in_g(T162))
U14_ag(T169, T162, T163, inA_out_g(T162)) → inG_out_ag(0, tree(s(T169), T162, T163))
inG_in_ag(s(T184), tree(s(T183), T162, T163)) → U15_ag(T184, T183, T162, T163, pF_in_agg(T184, T183, T162))
U15_ag(T184, T183, T162, T163, pF_out_agg(T184, T183, T162)) → inG_out_ag(s(T184), tree(s(T183), T162, T163))
inG_in_ag(T202, tree(T199, T200, T201)) → U16_ag(T202, T199, T200, T201, pH_in_gag(T199, T202, T201))
U16_ag(T202, T199, T200, T201, pH_out_gag(T199, T202, T201)) → inG_out_ag(T202, tree(T199, T200, T201))
inG_in_ag(s(T219), tree(0, T211, T212)) → U17_ag(T219, T211, T212, inG_in_ag(s(T219), T212))
inG_in_ag(s(T232), tree(s(T230), T211, T212)) → U18_ag(T232, T230, T211, T212, lessE_in_ga(T230, T232))
U18_ag(T232, T230, T211, T212, lessE_out_ga(T230, T232)) → inG_out_ag(s(T232), tree(s(T230), T211, T212))
inG_in_ag(s(T235), tree(s(T230), T211, T212)) → U19_ag(T235, T230, T211, T212, lessE_in_ga(T230, T235))
U19_ag(T235, T230, T211, T212, lessE_out_ga(T230, T235)) → U20_ag(T235, T230, T211, T212, inG_in_ag(s(T235), T212))
U20_ag(T235, T230, T211, T212, inG_out_ag(s(T235), T212)) → inG_out_ag(s(T235), tree(s(T230), T211, T212))
U17_ag(T219, T211, T212, inG_out_ag(s(T219), T212)) → inG_out_ag(s(T219), tree(0, T211, T212))
U10_gag(T127, T133, T129, inG_out_ag(T133, T129)) → pH_out_gag(T127, T133, T129)
U13_ag(T130, T127, T128, T129, pH_out_gag(T127, T130, T129)) → inG_out_ag(T130, tree(T127, T128, T129))
ING_IN_AG(0, tree(s(T22), T15, T16)) → U11_AG(T22, T15, T16, inA_in_g(T15))
ING_IN_AG(0, tree(s(T22), T15, T16)) → INA_IN_G(T15)
INA_IN_G(tree(T49, T50, T51)) → U1_G(T49, T50, T51, lessB_in_g(T49))
INA_IN_G(tree(T49, T50, T51)) → LESSB_IN_G(T49)
U1_G(T49, T50, T51, lessB_out_g(T49)) → U2_G(T49, T50, T51, inA_in_g(T50))
U1_G(T49, T50, T51, lessB_out_g(T49)) → INA_IN_G(T50)
ING_IN_AG(s(T89), tree(s(T88), T15, T16)) → U12_AG(T89, T88, T15, T16, pF_in_agg(T89, T88, T15))
ING_IN_AG(s(T89), tree(s(T88), T15, T16)) → PF_IN_AGG(T89, T88, T15)
PF_IN_AGG(T89, T88, T15) → U5_AGG(T89, T88, T15, lessD_in_ag(T89, T88))
PF_IN_AGG(T89, T88, T15) → LESSD_IN_AG(T89, T88)
LESSD_IN_AG(s(T106), s(T105)) → U3_AG(T106, T105, lessD_in_ag(T106, T105))
LESSD_IN_AG(s(T106), s(T105)) → LESSD_IN_AG(T106, T105)
PF_IN_AGG(T92, T88, T15) → U6_AGG(T92, T88, T15, lessD_in_ag(T92, T88))
U6_AGG(T92, T88, T15, lessD_out_ag(T92, T88)) → U7_AGG(T92, T88, T15, inG_in_gg(s(T92), T15))
U6_AGG(T92, T88, T15, lessD_out_ag(T92, T88)) → ING_IN_GG(s(T92), T15)
ING_IN_GG(0, tree(s(T22), T15, T16)) → U11_GG(T22, T15, T16, inA_in_g(T15))
ING_IN_GG(0, tree(s(T22), T15, T16)) → INA_IN_G(T15)
ING_IN_GG(s(T89), tree(s(T88), T15, T16)) → U12_GG(T89, T88, T15, T16, pF_in_ggg(T89, T88, T15))
ING_IN_GG(s(T89), tree(s(T88), T15, T16)) → PF_IN_GGG(T89, T88, T15)
PF_IN_GGG(T89, T88, T15) → U5_GGG(T89, T88, T15, lessD_in_gg(T89, T88))
PF_IN_GGG(T89, T88, T15) → LESSD_IN_GG(T89, T88)
LESSD_IN_GG(s(T106), s(T105)) → U3_GG(T106, T105, lessD_in_gg(T106, T105))
LESSD_IN_GG(s(T106), s(T105)) → LESSD_IN_GG(T106, T105)
PF_IN_GGG(T92, T88, T15) → U6_GGG(T92, T88, T15, lessD_in_gg(T92, T88))
U6_GGG(T92, T88, T15, lessD_out_gg(T92, T88)) → U7_GGG(T92, T88, T15, inG_in_gg(s(T92), T15))
U6_GGG(T92, T88, T15, lessD_out_gg(T92, T88)) → ING_IN_GG(s(T92), T15)
ING_IN_GG(T130, tree(T127, T128, T129)) → U13_GG(T130, T127, T128, T129, pH_in_ggg(T127, T130, T129))
ING_IN_GG(T130, tree(T127, T128, T129)) → PH_IN_GGG(T127, T130, T129)
PH_IN_GGG(T127, T130, T129) → U8_GGG(T127, T130, T129, lessE_in_gg(T127, T130))
PH_IN_GGG(T127, T130, T129) → LESSE_IN_GG(T127, T130)
LESSE_IN_GG(s(T145), s(T147)) → U4_GG(T145, T147, lessE_in_gg(T145, T147))
LESSE_IN_GG(s(T145), s(T147)) → LESSE_IN_GG(T145, T147)
PH_IN_GGG(T127, T133, T129) → U9_GGG(T127, T133, T129, lessE_in_gg(T127, T133))
U9_GGG(T127, T133, T129, lessE_out_gg(T127, T133)) → U10_GGG(T127, T133, T129, inG_in_gg(T133, T129))
U9_GGG(T127, T133, T129, lessE_out_gg(T127, T133)) → ING_IN_GG(T133, T129)
ING_IN_GG(0, tree(s(T169), T162, T163)) → U14_GG(T169, T162, T163, inA_in_g(T162))
ING_IN_GG(s(T184), tree(s(T183), T162, T163)) → U15_GG(T184, T183, T162, T163, pF_in_ggg(T184, T183, T162))
ING_IN_GG(T202, tree(T199, T200, T201)) → U16_GG(T202, T199, T200, T201, pH_in_ggg(T199, T202, T201))
ING_IN_GG(s(T219), tree(0, T211, T212)) → U17_GG(T219, T211, T212, inG_in_gg(s(T219), T212))
ING_IN_GG(s(T219), tree(0, T211, T212)) → ING_IN_GG(s(T219), T212)
ING_IN_GG(s(T232), tree(s(T230), T211, T212)) → U18_GG(T232, T230, T211, T212, lessE_in_gg(T230, T232))
ING_IN_GG(s(T232), tree(s(T230), T211, T212)) → LESSE_IN_GG(T230, T232)
ING_IN_GG(s(T235), tree(s(T230), T211, T212)) → U19_GG(T235, T230, T211, T212, lessE_in_gg(T230, T235))
U19_GG(T235, T230, T211, T212, lessE_out_gg(T230, T235)) → U20_GG(T235, T230, T211, T212, inG_in_gg(s(T235), T212))
U19_GG(T235, T230, T211, T212, lessE_out_gg(T230, T235)) → ING_IN_GG(s(T235), T212)
ING_IN_AG(T130, tree(T127, T128, T129)) → U13_AG(T130, T127, T128, T129, pH_in_gag(T127, T130, T129))
ING_IN_AG(T130, tree(T127, T128, T129)) → PH_IN_GAG(T127, T130, T129)
PH_IN_GAG(T127, T130, T129) → U8_GAG(T127, T130, T129, lessE_in_ga(T127, T130))
PH_IN_GAG(T127, T130, T129) → LESSE_IN_GA(T127, T130)
LESSE_IN_GA(s(T145), s(T147)) → U4_GA(T145, T147, lessE_in_ga(T145, T147))
LESSE_IN_GA(s(T145), s(T147)) → LESSE_IN_GA(T145, T147)
PH_IN_GAG(T127, T133, T129) → U9_GAG(T127, T133, T129, lessE_in_ga(T127, T133))
U9_GAG(T127, T133, T129, lessE_out_ga(T127, T133)) → U10_GAG(T127, T133, T129, inG_in_ag(T133, T129))
U9_GAG(T127, T133, T129, lessE_out_ga(T127, T133)) → ING_IN_AG(T133, T129)
ING_IN_AG(0, tree(s(T169), T162, T163)) → U14_AG(T169, T162, T163, inA_in_g(T162))
ING_IN_AG(s(T184), tree(s(T183), T162, T163)) → U15_AG(T184, T183, T162, T163, pF_in_agg(T184, T183, T162))
ING_IN_AG(T202, tree(T199, T200, T201)) → U16_AG(T202, T199, T200, T201, pH_in_gag(T199, T202, T201))
ING_IN_AG(s(T219), tree(0, T211, T212)) → U17_AG(T219, T211, T212, inG_in_ag(s(T219), T212))
ING_IN_AG(s(T219), tree(0, T211, T212)) → ING_IN_AG(s(T219), T212)
ING_IN_AG(s(T232), tree(s(T230), T211, T212)) → U18_AG(T232, T230, T211, T212, lessE_in_ga(T230, T232))
ING_IN_AG(s(T232), tree(s(T230), T211, T212)) → LESSE_IN_GA(T230, T232)
ING_IN_AG(s(T235), tree(s(T230), T211, T212)) → U19_AG(T235, T230, T211, T212, lessE_in_ga(T230, T235))
U19_AG(T235, T230, T211, T212, lessE_out_ga(T230, T235)) → U20_AG(T235, T230, T211, T212, inG_in_ag(s(T235), T212))
U19_AG(T235, T230, T211, T212, lessE_out_ga(T230, T235)) → ING_IN_AG(s(T235), T212)
inG_in_ag(T6, tree(T6, T7, T8)) → inG_out_ag(T6, tree(T6, T7, T8))
inG_in_ag(0, tree(s(T22), T15, T16)) → U11_ag(T22, T15, T16, inA_in_g(T15))
inA_in_g(tree(0, T35, T36)) → inA_out_g(tree(0, T35, T36))
inA_in_g(tree(T49, T50, T51)) → U1_g(T49, T50, T51, lessB_in_g(T49))
lessB_in_g(s(T60)) → lessB_out_g(s(T60))
U1_g(T49, T50, T51, lessB_out_g(T49)) → inA_out_g(tree(T49, T50, T51))
U1_g(T49, T50, T51, lessB_out_g(T49)) → U2_g(T49, T50, T51, inA_in_g(T50))
U2_g(T49, T50, T51, inA_out_g(T50)) → inA_out_g(tree(T49, T50, T51))
U11_ag(T22, T15, T16, inA_out_g(T15)) → inG_out_ag(0, tree(s(T22), T15, T16))
inG_in_ag(s(T89), tree(s(T88), T15, T16)) → U12_ag(T89, T88, T15, T16, pF_in_agg(T89, T88, T15))
pF_in_agg(T89, T88, T15) → U5_agg(T89, T88, T15, lessD_in_ag(T89, T88))
lessD_in_ag(0, s(T99)) → lessD_out_ag(0, s(T99))
lessD_in_ag(s(T106), s(T105)) → U3_ag(T106, T105, lessD_in_ag(T106, T105))
U3_ag(T106, T105, lessD_out_ag(T106, T105)) → lessD_out_ag(s(T106), s(T105))
U5_agg(T89, T88, T15, lessD_out_ag(T89, T88)) → pF_out_agg(T89, T88, T15)
pF_in_agg(T92, T88, T15) → U6_agg(T92, T88, T15, lessD_in_ag(T92, T88))
U6_agg(T92, T88, T15, lessD_out_ag(T92, T88)) → U7_agg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T6, tree(T6, T7, T8)) → inG_out_gg(T6, tree(T6, T7, T8))
inG_in_gg(0, tree(s(T22), T15, T16)) → U11_gg(T22, T15, T16, inA_in_g(T15))
U11_gg(T22, T15, T16, inA_out_g(T15)) → inG_out_gg(0, tree(s(T22), T15, T16))
inG_in_gg(s(T89), tree(s(T88), T15, T16)) → U12_gg(T89, T88, T15, T16, pF_in_ggg(T89, T88, T15))
pF_in_ggg(T89, T88, T15) → U5_ggg(T89, T88, T15, lessD_in_gg(T89, T88))
lessD_in_gg(0, s(T99)) → lessD_out_gg(0, s(T99))
lessD_in_gg(s(T106), s(T105)) → U3_gg(T106, T105, lessD_in_gg(T106, T105))
U3_gg(T106, T105, lessD_out_gg(T106, T105)) → lessD_out_gg(s(T106), s(T105))
U5_ggg(T89, T88, T15, lessD_out_gg(T89, T88)) → pF_out_ggg(T89, T88, T15)
pF_in_ggg(T92, T88, T15) → U6_ggg(T92, T88, T15, lessD_in_gg(T92, T88))
U6_ggg(T92, T88, T15, lessD_out_gg(T92, T88)) → U7_ggg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T130, tree(T127, T128, T129)) → U13_gg(T130, T127, T128, T129, pH_in_ggg(T127, T130, T129))
pH_in_ggg(T127, T130, T129) → U8_ggg(T127, T130, T129, lessE_in_gg(T127, T130))
lessE_in_gg(0, s(T140)) → lessE_out_gg(0, s(T140))
lessE_in_gg(s(T145), s(T147)) → U4_gg(T145, T147, lessE_in_gg(T145, T147))
U4_gg(T145, T147, lessE_out_gg(T145, T147)) → lessE_out_gg(s(T145), s(T147))
U8_ggg(T127, T130, T129, lessE_out_gg(T127, T130)) → pH_out_ggg(T127, T130, T129)
pH_in_ggg(T127, T133, T129) → U9_ggg(T127, T133, T129, lessE_in_gg(T127, T133))
U9_ggg(T127, T133, T129, lessE_out_gg(T127, T133)) → U10_ggg(T127, T133, T129, inG_in_gg(T133, T129))
inG_in_gg(0, tree(s(T169), T162, T163)) → U14_gg(T169, T162, T163, inA_in_g(T162))
U14_gg(T169, T162, T163, inA_out_g(T162)) → inG_out_gg(0, tree(s(T169), T162, T163))
inG_in_gg(s(T184), tree(s(T183), T162, T163)) → U15_gg(T184, T183, T162, T163, pF_in_ggg(T184, T183, T162))
U15_gg(T184, T183, T162, T163, pF_out_ggg(T184, T183, T162)) → inG_out_gg(s(T184), tree(s(T183), T162, T163))
inG_in_gg(T202, tree(T199, T200, T201)) → U16_gg(T202, T199, T200, T201, pH_in_ggg(T199, T202, T201))
U16_gg(T202, T199, T200, T201, pH_out_ggg(T199, T202, T201)) → inG_out_gg(T202, tree(T199, T200, T201))
inG_in_gg(s(T219), tree(0, T211, T212)) → U17_gg(T219, T211, T212, inG_in_gg(s(T219), T212))
inG_in_gg(s(T232), tree(s(T230), T211, T212)) → U18_gg(T232, T230, T211, T212, lessE_in_gg(T230, T232))
U18_gg(T232, T230, T211, T212, lessE_out_gg(T230, T232)) → inG_out_gg(s(T232), tree(s(T230), T211, T212))
inG_in_gg(s(T235), tree(s(T230), T211, T212)) → U19_gg(T235, T230, T211, T212, lessE_in_gg(T230, T235))
U19_gg(T235, T230, T211, T212, lessE_out_gg(T230, T235)) → U20_gg(T235, T230, T211, T212, inG_in_gg(s(T235), T212))
U20_gg(T235, T230, T211, T212, inG_out_gg(s(T235), T212)) → inG_out_gg(s(T235), tree(s(T230), T211, T212))
U17_gg(T219, T211, T212, inG_out_gg(s(T219), T212)) → inG_out_gg(s(T219), tree(0, T211, T212))
U10_ggg(T127, T133, T129, inG_out_gg(T133, T129)) → pH_out_ggg(T127, T133, T129)
U13_gg(T130, T127, T128, T129, pH_out_ggg(T127, T130, T129)) → inG_out_gg(T130, tree(T127, T128, T129))
U7_ggg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_ggg(T92, T88, T15)
U12_gg(T89, T88, T15, T16, pF_out_ggg(T89, T88, T15)) → inG_out_gg(s(T89), tree(s(T88), T15, T16))
U7_agg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_agg(T92, T88, T15)
U12_ag(T89, T88, T15, T16, pF_out_agg(T89, T88, T15)) → inG_out_ag(s(T89), tree(s(T88), T15, T16))
inG_in_ag(T130, tree(T127, T128, T129)) → U13_ag(T130, T127, T128, T129, pH_in_gag(T127, T130, T129))
pH_in_gag(T127, T130, T129) → U8_gag(T127, T130, T129, lessE_in_ga(T127, T130))
lessE_in_ga(0, s(T140)) → lessE_out_ga(0, s(T140))
lessE_in_ga(s(T145), s(T147)) → U4_ga(T145, T147, lessE_in_ga(T145, T147))
U4_ga(T145, T147, lessE_out_ga(T145, T147)) → lessE_out_ga(s(T145), s(T147))
U8_gag(T127, T130, T129, lessE_out_ga(T127, T130)) → pH_out_gag(T127, T130, T129)
pH_in_gag(T127, T133, T129) → U9_gag(T127, T133, T129, lessE_in_ga(T127, T133))
U9_gag(T127, T133, T129, lessE_out_ga(T127, T133)) → U10_gag(T127, T133, T129, inG_in_ag(T133, T129))
inG_in_ag(0, tree(s(T169), T162, T163)) → U14_ag(T169, T162, T163, inA_in_g(T162))
U14_ag(T169, T162, T163, inA_out_g(T162)) → inG_out_ag(0, tree(s(T169), T162, T163))
inG_in_ag(s(T184), tree(s(T183), T162, T163)) → U15_ag(T184, T183, T162, T163, pF_in_agg(T184, T183, T162))
U15_ag(T184, T183, T162, T163, pF_out_agg(T184, T183, T162)) → inG_out_ag(s(T184), tree(s(T183), T162, T163))
inG_in_ag(T202, tree(T199, T200, T201)) → U16_ag(T202, T199, T200, T201, pH_in_gag(T199, T202, T201))
U16_ag(T202, T199, T200, T201, pH_out_gag(T199, T202, T201)) → inG_out_ag(T202, tree(T199, T200, T201))
inG_in_ag(s(T219), tree(0, T211, T212)) → U17_ag(T219, T211, T212, inG_in_ag(s(T219), T212))
inG_in_ag(s(T232), tree(s(T230), T211, T212)) → U18_ag(T232, T230, T211, T212, lessE_in_ga(T230, T232))
U18_ag(T232, T230, T211, T212, lessE_out_ga(T230, T232)) → inG_out_ag(s(T232), tree(s(T230), T211, T212))
inG_in_ag(s(T235), tree(s(T230), T211, T212)) → U19_ag(T235, T230, T211, T212, lessE_in_ga(T230, T235))
U19_ag(T235, T230, T211, T212, lessE_out_ga(T230, T235)) → U20_ag(T235, T230, T211, T212, inG_in_ag(s(T235), T212))
U20_ag(T235, T230, T211, T212, inG_out_ag(s(T235), T212)) → inG_out_ag(s(T235), tree(s(T230), T211, T212))
U17_ag(T219, T211, T212, inG_out_ag(s(T219), T212)) → inG_out_ag(s(T219), tree(0, T211, T212))
U10_gag(T127, T133, T129, inG_out_ag(T133, T129)) → pH_out_gag(T127, T133, T129)
U13_ag(T130, T127, T128, T129, pH_out_gag(T127, T130, T129)) → inG_out_ag(T130, tree(T127, T128, T129))
LESSE_IN_GA(s(T145), s(T147)) → LESSE_IN_GA(T145, T147)
inG_in_ag(T6, tree(T6, T7, T8)) → inG_out_ag(T6, tree(T6, T7, T8))
inG_in_ag(0, tree(s(T22), T15, T16)) → U11_ag(T22, T15, T16, inA_in_g(T15))
inA_in_g(tree(0, T35, T36)) → inA_out_g(tree(0, T35, T36))
inA_in_g(tree(T49, T50, T51)) → U1_g(T49, T50, T51, lessB_in_g(T49))
lessB_in_g(s(T60)) → lessB_out_g(s(T60))
U1_g(T49, T50, T51, lessB_out_g(T49)) → inA_out_g(tree(T49, T50, T51))
U1_g(T49, T50, T51, lessB_out_g(T49)) → U2_g(T49, T50, T51, inA_in_g(T50))
U2_g(T49, T50, T51, inA_out_g(T50)) → inA_out_g(tree(T49, T50, T51))
U11_ag(T22, T15, T16, inA_out_g(T15)) → inG_out_ag(0, tree(s(T22), T15, T16))
inG_in_ag(s(T89), tree(s(T88), T15, T16)) → U12_ag(T89, T88, T15, T16, pF_in_agg(T89, T88, T15))
pF_in_agg(T89, T88, T15) → U5_agg(T89, T88, T15, lessD_in_ag(T89, T88))
lessD_in_ag(0, s(T99)) → lessD_out_ag(0, s(T99))
lessD_in_ag(s(T106), s(T105)) → U3_ag(T106, T105, lessD_in_ag(T106, T105))
U3_ag(T106, T105, lessD_out_ag(T106, T105)) → lessD_out_ag(s(T106), s(T105))
U5_agg(T89, T88, T15, lessD_out_ag(T89, T88)) → pF_out_agg(T89, T88, T15)
pF_in_agg(T92, T88, T15) → U6_agg(T92, T88, T15, lessD_in_ag(T92, T88))
U6_agg(T92, T88, T15, lessD_out_ag(T92, T88)) → U7_agg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T6, tree(T6, T7, T8)) → inG_out_gg(T6, tree(T6, T7, T8))
inG_in_gg(0, tree(s(T22), T15, T16)) → U11_gg(T22, T15, T16, inA_in_g(T15))
U11_gg(T22, T15, T16, inA_out_g(T15)) → inG_out_gg(0, tree(s(T22), T15, T16))
inG_in_gg(s(T89), tree(s(T88), T15, T16)) → U12_gg(T89, T88, T15, T16, pF_in_ggg(T89, T88, T15))
pF_in_ggg(T89, T88, T15) → U5_ggg(T89, T88, T15, lessD_in_gg(T89, T88))
lessD_in_gg(0, s(T99)) → lessD_out_gg(0, s(T99))
lessD_in_gg(s(T106), s(T105)) → U3_gg(T106, T105, lessD_in_gg(T106, T105))
U3_gg(T106, T105, lessD_out_gg(T106, T105)) → lessD_out_gg(s(T106), s(T105))
U5_ggg(T89, T88, T15, lessD_out_gg(T89, T88)) → pF_out_ggg(T89, T88, T15)
pF_in_ggg(T92, T88, T15) → U6_ggg(T92, T88, T15, lessD_in_gg(T92, T88))
U6_ggg(T92, T88, T15, lessD_out_gg(T92, T88)) → U7_ggg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T130, tree(T127, T128, T129)) → U13_gg(T130, T127, T128, T129, pH_in_ggg(T127, T130, T129))
pH_in_ggg(T127, T130, T129) → U8_ggg(T127, T130, T129, lessE_in_gg(T127, T130))
lessE_in_gg(0, s(T140)) → lessE_out_gg(0, s(T140))
lessE_in_gg(s(T145), s(T147)) → U4_gg(T145, T147, lessE_in_gg(T145, T147))
U4_gg(T145, T147, lessE_out_gg(T145, T147)) → lessE_out_gg(s(T145), s(T147))
U8_ggg(T127, T130, T129, lessE_out_gg(T127, T130)) → pH_out_ggg(T127, T130, T129)
pH_in_ggg(T127, T133, T129) → U9_ggg(T127, T133, T129, lessE_in_gg(T127, T133))
U9_ggg(T127, T133, T129, lessE_out_gg(T127, T133)) → U10_ggg(T127, T133, T129, inG_in_gg(T133, T129))
inG_in_gg(0, tree(s(T169), T162, T163)) → U14_gg(T169, T162, T163, inA_in_g(T162))
U14_gg(T169, T162, T163, inA_out_g(T162)) → inG_out_gg(0, tree(s(T169), T162, T163))
inG_in_gg(s(T184), tree(s(T183), T162, T163)) → U15_gg(T184, T183, T162, T163, pF_in_ggg(T184, T183, T162))
U15_gg(T184, T183, T162, T163, pF_out_ggg(T184, T183, T162)) → inG_out_gg(s(T184), tree(s(T183), T162, T163))
inG_in_gg(T202, tree(T199, T200, T201)) → U16_gg(T202, T199, T200, T201, pH_in_ggg(T199, T202, T201))
U16_gg(T202, T199, T200, T201, pH_out_ggg(T199, T202, T201)) → inG_out_gg(T202, tree(T199, T200, T201))
inG_in_gg(s(T219), tree(0, T211, T212)) → U17_gg(T219, T211, T212, inG_in_gg(s(T219), T212))
inG_in_gg(s(T232), tree(s(T230), T211, T212)) → U18_gg(T232, T230, T211, T212, lessE_in_gg(T230, T232))
U18_gg(T232, T230, T211, T212, lessE_out_gg(T230, T232)) → inG_out_gg(s(T232), tree(s(T230), T211, T212))
inG_in_gg(s(T235), tree(s(T230), T211, T212)) → U19_gg(T235, T230, T211, T212, lessE_in_gg(T230, T235))
U19_gg(T235, T230, T211, T212, lessE_out_gg(T230, T235)) → U20_gg(T235, T230, T211, T212, inG_in_gg(s(T235), T212))
U20_gg(T235, T230, T211, T212, inG_out_gg(s(T235), T212)) → inG_out_gg(s(T235), tree(s(T230), T211, T212))
U17_gg(T219, T211, T212, inG_out_gg(s(T219), T212)) → inG_out_gg(s(T219), tree(0, T211, T212))
U10_ggg(T127, T133, T129, inG_out_gg(T133, T129)) → pH_out_ggg(T127, T133, T129)
U13_gg(T130, T127, T128, T129, pH_out_ggg(T127, T130, T129)) → inG_out_gg(T130, tree(T127, T128, T129))
U7_ggg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_ggg(T92, T88, T15)
U12_gg(T89, T88, T15, T16, pF_out_ggg(T89, T88, T15)) → inG_out_gg(s(T89), tree(s(T88), T15, T16))
U7_agg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_agg(T92, T88, T15)
U12_ag(T89, T88, T15, T16, pF_out_agg(T89, T88, T15)) → inG_out_ag(s(T89), tree(s(T88), T15, T16))
inG_in_ag(T130, tree(T127, T128, T129)) → U13_ag(T130, T127, T128, T129, pH_in_gag(T127, T130, T129))
pH_in_gag(T127, T130, T129) → U8_gag(T127, T130, T129, lessE_in_ga(T127, T130))
lessE_in_ga(0, s(T140)) → lessE_out_ga(0, s(T140))
lessE_in_ga(s(T145), s(T147)) → U4_ga(T145, T147, lessE_in_ga(T145, T147))
U4_ga(T145, T147, lessE_out_ga(T145, T147)) → lessE_out_ga(s(T145), s(T147))
U8_gag(T127, T130, T129, lessE_out_ga(T127, T130)) → pH_out_gag(T127, T130, T129)
pH_in_gag(T127, T133, T129) → U9_gag(T127, T133, T129, lessE_in_ga(T127, T133))
U9_gag(T127, T133, T129, lessE_out_ga(T127, T133)) → U10_gag(T127, T133, T129, inG_in_ag(T133, T129))
inG_in_ag(0, tree(s(T169), T162, T163)) → U14_ag(T169, T162, T163, inA_in_g(T162))
U14_ag(T169, T162, T163, inA_out_g(T162)) → inG_out_ag(0, tree(s(T169), T162, T163))
inG_in_ag(s(T184), tree(s(T183), T162, T163)) → U15_ag(T184, T183, T162, T163, pF_in_agg(T184, T183, T162))
U15_ag(T184, T183, T162, T163, pF_out_agg(T184, T183, T162)) → inG_out_ag(s(T184), tree(s(T183), T162, T163))
inG_in_ag(T202, tree(T199, T200, T201)) → U16_ag(T202, T199, T200, T201, pH_in_gag(T199, T202, T201))
U16_ag(T202, T199, T200, T201, pH_out_gag(T199, T202, T201)) → inG_out_ag(T202, tree(T199, T200, T201))
inG_in_ag(s(T219), tree(0, T211, T212)) → U17_ag(T219, T211, T212, inG_in_ag(s(T219), T212))
inG_in_ag(s(T232), tree(s(T230), T211, T212)) → U18_ag(T232, T230, T211, T212, lessE_in_ga(T230, T232))
U18_ag(T232, T230, T211, T212, lessE_out_ga(T230, T232)) → inG_out_ag(s(T232), tree(s(T230), T211, T212))
inG_in_ag(s(T235), tree(s(T230), T211, T212)) → U19_ag(T235, T230, T211, T212, lessE_in_ga(T230, T235))
U19_ag(T235, T230, T211, T212, lessE_out_ga(T230, T235)) → U20_ag(T235, T230, T211, T212, inG_in_ag(s(T235), T212))
U20_ag(T235, T230, T211, T212, inG_out_ag(s(T235), T212)) → inG_out_ag(s(T235), tree(s(T230), T211, T212))
U17_ag(T219, T211, T212, inG_out_ag(s(T219), T212)) → inG_out_ag(s(T219), tree(0, T211, T212))
U10_gag(T127, T133, T129, inG_out_ag(T133, T129)) → pH_out_gag(T127, T133, T129)
U13_ag(T130, T127, T128, T129, pH_out_gag(T127, T130, T129)) → inG_out_ag(T130, tree(T127, T128, T129))
LESSE_IN_GA(s(T145), s(T147)) → LESSE_IN_GA(T145, T147)
LESSE_IN_GA(s(T145)) → LESSE_IN_GA(T145)
From the DPs we obtained the following set of size-change graphs:
LESSE_IN_GG(s(T145), s(T147)) → LESSE_IN_GG(T145, T147)
inG_in_ag(T6, tree(T6, T7, T8)) → inG_out_ag(T6, tree(T6, T7, T8))
inG_in_ag(0, tree(s(T22), T15, T16)) → U11_ag(T22, T15, T16, inA_in_g(T15))
inA_in_g(tree(0, T35, T36)) → inA_out_g(tree(0, T35, T36))
inA_in_g(tree(T49, T50, T51)) → U1_g(T49, T50, T51, lessB_in_g(T49))
lessB_in_g(s(T60)) → lessB_out_g(s(T60))
U1_g(T49, T50, T51, lessB_out_g(T49)) → inA_out_g(tree(T49, T50, T51))
U1_g(T49, T50, T51, lessB_out_g(T49)) → U2_g(T49, T50, T51, inA_in_g(T50))
U2_g(T49, T50, T51, inA_out_g(T50)) → inA_out_g(tree(T49, T50, T51))
U11_ag(T22, T15, T16, inA_out_g(T15)) → inG_out_ag(0, tree(s(T22), T15, T16))
inG_in_ag(s(T89), tree(s(T88), T15, T16)) → U12_ag(T89, T88, T15, T16, pF_in_agg(T89, T88, T15))
pF_in_agg(T89, T88, T15) → U5_agg(T89, T88, T15, lessD_in_ag(T89, T88))
lessD_in_ag(0, s(T99)) → lessD_out_ag(0, s(T99))
lessD_in_ag(s(T106), s(T105)) → U3_ag(T106, T105, lessD_in_ag(T106, T105))
U3_ag(T106, T105, lessD_out_ag(T106, T105)) → lessD_out_ag(s(T106), s(T105))
U5_agg(T89, T88, T15, lessD_out_ag(T89, T88)) → pF_out_agg(T89, T88, T15)
pF_in_agg(T92, T88, T15) → U6_agg(T92, T88, T15, lessD_in_ag(T92, T88))
U6_agg(T92, T88, T15, lessD_out_ag(T92, T88)) → U7_agg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T6, tree(T6, T7, T8)) → inG_out_gg(T6, tree(T6, T7, T8))
inG_in_gg(0, tree(s(T22), T15, T16)) → U11_gg(T22, T15, T16, inA_in_g(T15))
U11_gg(T22, T15, T16, inA_out_g(T15)) → inG_out_gg(0, tree(s(T22), T15, T16))
inG_in_gg(s(T89), tree(s(T88), T15, T16)) → U12_gg(T89, T88, T15, T16, pF_in_ggg(T89, T88, T15))
pF_in_ggg(T89, T88, T15) → U5_ggg(T89, T88, T15, lessD_in_gg(T89, T88))
lessD_in_gg(0, s(T99)) → lessD_out_gg(0, s(T99))
lessD_in_gg(s(T106), s(T105)) → U3_gg(T106, T105, lessD_in_gg(T106, T105))
U3_gg(T106, T105, lessD_out_gg(T106, T105)) → lessD_out_gg(s(T106), s(T105))
U5_ggg(T89, T88, T15, lessD_out_gg(T89, T88)) → pF_out_ggg(T89, T88, T15)
pF_in_ggg(T92, T88, T15) → U6_ggg(T92, T88, T15, lessD_in_gg(T92, T88))
U6_ggg(T92, T88, T15, lessD_out_gg(T92, T88)) → U7_ggg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T130, tree(T127, T128, T129)) → U13_gg(T130, T127, T128, T129, pH_in_ggg(T127, T130, T129))
pH_in_ggg(T127, T130, T129) → U8_ggg(T127, T130, T129, lessE_in_gg(T127, T130))
lessE_in_gg(0, s(T140)) → lessE_out_gg(0, s(T140))
lessE_in_gg(s(T145), s(T147)) → U4_gg(T145, T147, lessE_in_gg(T145, T147))
U4_gg(T145, T147, lessE_out_gg(T145, T147)) → lessE_out_gg(s(T145), s(T147))
U8_ggg(T127, T130, T129, lessE_out_gg(T127, T130)) → pH_out_ggg(T127, T130, T129)
pH_in_ggg(T127, T133, T129) → U9_ggg(T127, T133, T129, lessE_in_gg(T127, T133))
U9_ggg(T127, T133, T129, lessE_out_gg(T127, T133)) → U10_ggg(T127, T133, T129, inG_in_gg(T133, T129))
inG_in_gg(0, tree(s(T169), T162, T163)) → U14_gg(T169, T162, T163, inA_in_g(T162))
U14_gg(T169, T162, T163, inA_out_g(T162)) → inG_out_gg(0, tree(s(T169), T162, T163))
inG_in_gg(s(T184), tree(s(T183), T162, T163)) → U15_gg(T184, T183, T162, T163, pF_in_ggg(T184, T183, T162))
U15_gg(T184, T183, T162, T163, pF_out_ggg(T184, T183, T162)) → inG_out_gg(s(T184), tree(s(T183), T162, T163))
inG_in_gg(T202, tree(T199, T200, T201)) → U16_gg(T202, T199, T200, T201, pH_in_ggg(T199, T202, T201))
U16_gg(T202, T199, T200, T201, pH_out_ggg(T199, T202, T201)) → inG_out_gg(T202, tree(T199, T200, T201))
inG_in_gg(s(T219), tree(0, T211, T212)) → U17_gg(T219, T211, T212, inG_in_gg(s(T219), T212))
inG_in_gg(s(T232), tree(s(T230), T211, T212)) → U18_gg(T232, T230, T211, T212, lessE_in_gg(T230, T232))
U18_gg(T232, T230, T211, T212, lessE_out_gg(T230, T232)) → inG_out_gg(s(T232), tree(s(T230), T211, T212))
inG_in_gg(s(T235), tree(s(T230), T211, T212)) → U19_gg(T235, T230, T211, T212, lessE_in_gg(T230, T235))
U19_gg(T235, T230, T211, T212, lessE_out_gg(T230, T235)) → U20_gg(T235, T230, T211, T212, inG_in_gg(s(T235), T212))
U20_gg(T235, T230, T211, T212, inG_out_gg(s(T235), T212)) → inG_out_gg(s(T235), tree(s(T230), T211, T212))
U17_gg(T219, T211, T212, inG_out_gg(s(T219), T212)) → inG_out_gg(s(T219), tree(0, T211, T212))
U10_ggg(T127, T133, T129, inG_out_gg(T133, T129)) → pH_out_ggg(T127, T133, T129)
U13_gg(T130, T127, T128, T129, pH_out_ggg(T127, T130, T129)) → inG_out_gg(T130, tree(T127, T128, T129))
U7_ggg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_ggg(T92, T88, T15)
U12_gg(T89, T88, T15, T16, pF_out_ggg(T89, T88, T15)) → inG_out_gg(s(T89), tree(s(T88), T15, T16))
U7_agg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_agg(T92, T88, T15)
U12_ag(T89, T88, T15, T16, pF_out_agg(T89, T88, T15)) → inG_out_ag(s(T89), tree(s(T88), T15, T16))
inG_in_ag(T130, tree(T127, T128, T129)) → U13_ag(T130, T127, T128, T129, pH_in_gag(T127, T130, T129))
pH_in_gag(T127, T130, T129) → U8_gag(T127, T130, T129, lessE_in_ga(T127, T130))
lessE_in_ga(0, s(T140)) → lessE_out_ga(0, s(T140))
lessE_in_ga(s(T145), s(T147)) → U4_ga(T145, T147, lessE_in_ga(T145, T147))
U4_ga(T145, T147, lessE_out_ga(T145, T147)) → lessE_out_ga(s(T145), s(T147))
U8_gag(T127, T130, T129, lessE_out_ga(T127, T130)) → pH_out_gag(T127, T130, T129)
pH_in_gag(T127, T133, T129) → U9_gag(T127, T133, T129, lessE_in_ga(T127, T133))
U9_gag(T127, T133, T129, lessE_out_ga(T127, T133)) → U10_gag(T127, T133, T129, inG_in_ag(T133, T129))
inG_in_ag(0, tree(s(T169), T162, T163)) → U14_ag(T169, T162, T163, inA_in_g(T162))
U14_ag(T169, T162, T163, inA_out_g(T162)) → inG_out_ag(0, tree(s(T169), T162, T163))
inG_in_ag(s(T184), tree(s(T183), T162, T163)) → U15_ag(T184, T183, T162, T163, pF_in_agg(T184, T183, T162))
U15_ag(T184, T183, T162, T163, pF_out_agg(T184, T183, T162)) → inG_out_ag(s(T184), tree(s(T183), T162, T163))
inG_in_ag(T202, tree(T199, T200, T201)) → U16_ag(T202, T199, T200, T201, pH_in_gag(T199, T202, T201))
U16_ag(T202, T199, T200, T201, pH_out_gag(T199, T202, T201)) → inG_out_ag(T202, tree(T199, T200, T201))
inG_in_ag(s(T219), tree(0, T211, T212)) → U17_ag(T219, T211, T212, inG_in_ag(s(T219), T212))
inG_in_ag(s(T232), tree(s(T230), T211, T212)) → U18_ag(T232, T230, T211, T212, lessE_in_ga(T230, T232))
U18_ag(T232, T230, T211, T212, lessE_out_ga(T230, T232)) → inG_out_ag(s(T232), tree(s(T230), T211, T212))
inG_in_ag(s(T235), tree(s(T230), T211, T212)) → U19_ag(T235, T230, T211, T212, lessE_in_ga(T230, T235))
U19_ag(T235, T230, T211, T212, lessE_out_ga(T230, T235)) → U20_ag(T235, T230, T211, T212, inG_in_ag(s(T235), T212))
U20_ag(T235, T230, T211, T212, inG_out_ag(s(T235), T212)) → inG_out_ag(s(T235), tree(s(T230), T211, T212))
U17_ag(T219, T211, T212, inG_out_ag(s(T219), T212)) → inG_out_ag(s(T219), tree(0, T211, T212))
U10_gag(T127, T133, T129, inG_out_ag(T133, T129)) → pH_out_gag(T127, T133, T129)
U13_ag(T130, T127, T128, T129, pH_out_gag(T127, T130, T129)) → inG_out_ag(T130, tree(T127, T128, T129))
LESSE_IN_GG(s(T145), s(T147)) → LESSE_IN_GG(T145, T147)
LESSE_IN_GG(s(T145), s(T147)) → LESSE_IN_GG(T145, T147)
From the DPs we obtained the following set of size-change graphs:
LESSD_IN_GG(s(T106), s(T105)) → LESSD_IN_GG(T106, T105)
inG_in_ag(T6, tree(T6, T7, T8)) → inG_out_ag(T6, tree(T6, T7, T8))
inG_in_ag(0, tree(s(T22), T15, T16)) → U11_ag(T22, T15, T16, inA_in_g(T15))
inA_in_g(tree(0, T35, T36)) → inA_out_g(tree(0, T35, T36))
inA_in_g(tree(T49, T50, T51)) → U1_g(T49, T50, T51, lessB_in_g(T49))
lessB_in_g(s(T60)) → lessB_out_g(s(T60))
U1_g(T49, T50, T51, lessB_out_g(T49)) → inA_out_g(tree(T49, T50, T51))
U1_g(T49, T50, T51, lessB_out_g(T49)) → U2_g(T49, T50, T51, inA_in_g(T50))
U2_g(T49, T50, T51, inA_out_g(T50)) → inA_out_g(tree(T49, T50, T51))
U11_ag(T22, T15, T16, inA_out_g(T15)) → inG_out_ag(0, tree(s(T22), T15, T16))
inG_in_ag(s(T89), tree(s(T88), T15, T16)) → U12_ag(T89, T88, T15, T16, pF_in_agg(T89, T88, T15))
pF_in_agg(T89, T88, T15) → U5_agg(T89, T88, T15, lessD_in_ag(T89, T88))
lessD_in_ag(0, s(T99)) → lessD_out_ag(0, s(T99))
lessD_in_ag(s(T106), s(T105)) → U3_ag(T106, T105, lessD_in_ag(T106, T105))
U3_ag(T106, T105, lessD_out_ag(T106, T105)) → lessD_out_ag(s(T106), s(T105))
U5_agg(T89, T88, T15, lessD_out_ag(T89, T88)) → pF_out_agg(T89, T88, T15)
pF_in_agg(T92, T88, T15) → U6_agg(T92, T88, T15, lessD_in_ag(T92, T88))
U6_agg(T92, T88, T15, lessD_out_ag(T92, T88)) → U7_agg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T6, tree(T6, T7, T8)) → inG_out_gg(T6, tree(T6, T7, T8))
inG_in_gg(0, tree(s(T22), T15, T16)) → U11_gg(T22, T15, T16, inA_in_g(T15))
U11_gg(T22, T15, T16, inA_out_g(T15)) → inG_out_gg(0, tree(s(T22), T15, T16))
inG_in_gg(s(T89), tree(s(T88), T15, T16)) → U12_gg(T89, T88, T15, T16, pF_in_ggg(T89, T88, T15))
pF_in_ggg(T89, T88, T15) → U5_ggg(T89, T88, T15, lessD_in_gg(T89, T88))
lessD_in_gg(0, s(T99)) → lessD_out_gg(0, s(T99))
lessD_in_gg(s(T106), s(T105)) → U3_gg(T106, T105, lessD_in_gg(T106, T105))
U3_gg(T106, T105, lessD_out_gg(T106, T105)) → lessD_out_gg(s(T106), s(T105))
U5_ggg(T89, T88, T15, lessD_out_gg(T89, T88)) → pF_out_ggg(T89, T88, T15)
pF_in_ggg(T92, T88, T15) → U6_ggg(T92, T88, T15, lessD_in_gg(T92, T88))
U6_ggg(T92, T88, T15, lessD_out_gg(T92, T88)) → U7_ggg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T130, tree(T127, T128, T129)) → U13_gg(T130, T127, T128, T129, pH_in_ggg(T127, T130, T129))
pH_in_ggg(T127, T130, T129) → U8_ggg(T127, T130, T129, lessE_in_gg(T127, T130))
lessE_in_gg(0, s(T140)) → lessE_out_gg(0, s(T140))
lessE_in_gg(s(T145), s(T147)) → U4_gg(T145, T147, lessE_in_gg(T145, T147))
U4_gg(T145, T147, lessE_out_gg(T145, T147)) → lessE_out_gg(s(T145), s(T147))
U8_ggg(T127, T130, T129, lessE_out_gg(T127, T130)) → pH_out_ggg(T127, T130, T129)
pH_in_ggg(T127, T133, T129) → U9_ggg(T127, T133, T129, lessE_in_gg(T127, T133))
U9_ggg(T127, T133, T129, lessE_out_gg(T127, T133)) → U10_ggg(T127, T133, T129, inG_in_gg(T133, T129))
inG_in_gg(0, tree(s(T169), T162, T163)) → U14_gg(T169, T162, T163, inA_in_g(T162))
U14_gg(T169, T162, T163, inA_out_g(T162)) → inG_out_gg(0, tree(s(T169), T162, T163))
inG_in_gg(s(T184), tree(s(T183), T162, T163)) → U15_gg(T184, T183, T162, T163, pF_in_ggg(T184, T183, T162))
U15_gg(T184, T183, T162, T163, pF_out_ggg(T184, T183, T162)) → inG_out_gg(s(T184), tree(s(T183), T162, T163))
inG_in_gg(T202, tree(T199, T200, T201)) → U16_gg(T202, T199, T200, T201, pH_in_ggg(T199, T202, T201))
U16_gg(T202, T199, T200, T201, pH_out_ggg(T199, T202, T201)) → inG_out_gg(T202, tree(T199, T200, T201))
inG_in_gg(s(T219), tree(0, T211, T212)) → U17_gg(T219, T211, T212, inG_in_gg(s(T219), T212))
inG_in_gg(s(T232), tree(s(T230), T211, T212)) → U18_gg(T232, T230, T211, T212, lessE_in_gg(T230, T232))
U18_gg(T232, T230, T211, T212, lessE_out_gg(T230, T232)) → inG_out_gg(s(T232), tree(s(T230), T211, T212))
inG_in_gg(s(T235), tree(s(T230), T211, T212)) → U19_gg(T235, T230, T211, T212, lessE_in_gg(T230, T235))
U19_gg(T235, T230, T211, T212, lessE_out_gg(T230, T235)) → U20_gg(T235, T230, T211, T212, inG_in_gg(s(T235), T212))
U20_gg(T235, T230, T211, T212, inG_out_gg(s(T235), T212)) → inG_out_gg(s(T235), tree(s(T230), T211, T212))
U17_gg(T219, T211, T212, inG_out_gg(s(T219), T212)) → inG_out_gg(s(T219), tree(0, T211, T212))
U10_ggg(T127, T133, T129, inG_out_gg(T133, T129)) → pH_out_ggg(T127, T133, T129)
U13_gg(T130, T127, T128, T129, pH_out_ggg(T127, T130, T129)) → inG_out_gg(T130, tree(T127, T128, T129))
U7_ggg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_ggg(T92, T88, T15)
U12_gg(T89, T88, T15, T16, pF_out_ggg(T89, T88, T15)) → inG_out_gg(s(T89), tree(s(T88), T15, T16))
U7_agg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_agg(T92, T88, T15)
U12_ag(T89, T88, T15, T16, pF_out_agg(T89, T88, T15)) → inG_out_ag(s(T89), tree(s(T88), T15, T16))
inG_in_ag(T130, tree(T127, T128, T129)) → U13_ag(T130, T127, T128, T129, pH_in_gag(T127, T130, T129))
pH_in_gag(T127, T130, T129) → U8_gag(T127, T130, T129, lessE_in_ga(T127, T130))
lessE_in_ga(0, s(T140)) → lessE_out_ga(0, s(T140))
lessE_in_ga(s(T145), s(T147)) → U4_ga(T145, T147, lessE_in_ga(T145, T147))
U4_ga(T145, T147, lessE_out_ga(T145, T147)) → lessE_out_ga(s(T145), s(T147))
U8_gag(T127, T130, T129, lessE_out_ga(T127, T130)) → pH_out_gag(T127, T130, T129)
pH_in_gag(T127, T133, T129) → U9_gag(T127, T133, T129, lessE_in_ga(T127, T133))
U9_gag(T127, T133, T129, lessE_out_ga(T127, T133)) → U10_gag(T127, T133, T129, inG_in_ag(T133, T129))
inG_in_ag(0, tree(s(T169), T162, T163)) → U14_ag(T169, T162, T163, inA_in_g(T162))
U14_ag(T169, T162, T163, inA_out_g(T162)) → inG_out_ag(0, tree(s(T169), T162, T163))
inG_in_ag(s(T184), tree(s(T183), T162, T163)) → U15_ag(T184, T183, T162, T163, pF_in_agg(T184, T183, T162))
U15_ag(T184, T183, T162, T163, pF_out_agg(T184, T183, T162)) → inG_out_ag(s(T184), tree(s(T183), T162, T163))
inG_in_ag(T202, tree(T199, T200, T201)) → U16_ag(T202, T199, T200, T201, pH_in_gag(T199, T202, T201))
U16_ag(T202, T199, T200, T201, pH_out_gag(T199, T202, T201)) → inG_out_ag(T202, tree(T199, T200, T201))
inG_in_ag(s(T219), tree(0, T211, T212)) → U17_ag(T219, T211, T212, inG_in_ag(s(T219), T212))
inG_in_ag(s(T232), tree(s(T230), T211, T212)) → U18_ag(T232, T230, T211, T212, lessE_in_ga(T230, T232))
U18_ag(T232, T230, T211, T212, lessE_out_ga(T230, T232)) → inG_out_ag(s(T232), tree(s(T230), T211, T212))
inG_in_ag(s(T235), tree(s(T230), T211, T212)) → U19_ag(T235, T230, T211, T212, lessE_in_ga(T230, T235))
U19_ag(T235, T230, T211, T212, lessE_out_ga(T230, T235)) → U20_ag(T235, T230, T211, T212, inG_in_ag(s(T235), T212))
U20_ag(T235, T230, T211, T212, inG_out_ag(s(T235), T212)) → inG_out_ag(s(T235), tree(s(T230), T211, T212))
U17_ag(T219, T211, T212, inG_out_ag(s(T219), T212)) → inG_out_ag(s(T219), tree(0, T211, T212))
U10_gag(T127, T133, T129, inG_out_ag(T133, T129)) → pH_out_gag(T127, T133, T129)
U13_ag(T130, T127, T128, T129, pH_out_gag(T127, T130, T129)) → inG_out_ag(T130, tree(T127, T128, T129))
LESSD_IN_GG(s(T106), s(T105)) → LESSD_IN_GG(T106, T105)
LESSD_IN_GG(s(T106), s(T105)) → LESSD_IN_GG(T106, T105)
From the DPs we obtained the following set of size-change graphs:
LESSD_IN_AG(s(T106), s(T105)) → LESSD_IN_AG(T106, T105)
inG_in_ag(T6, tree(T6, T7, T8)) → inG_out_ag(T6, tree(T6, T7, T8))
inG_in_ag(0, tree(s(T22), T15, T16)) → U11_ag(T22, T15, T16, inA_in_g(T15))
inA_in_g(tree(0, T35, T36)) → inA_out_g(tree(0, T35, T36))
inA_in_g(tree(T49, T50, T51)) → U1_g(T49, T50, T51, lessB_in_g(T49))
lessB_in_g(s(T60)) → lessB_out_g(s(T60))
U1_g(T49, T50, T51, lessB_out_g(T49)) → inA_out_g(tree(T49, T50, T51))
U1_g(T49, T50, T51, lessB_out_g(T49)) → U2_g(T49, T50, T51, inA_in_g(T50))
U2_g(T49, T50, T51, inA_out_g(T50)) → inA_out_g(tree(T49, T50, T51))
U11_ag(T22, T15, T16, inA_out_g(T15)) → inG_out_ag(0, tree(s(T22), T15, T16))
inG_in_ag(s(T89), tree(s(T88), T15, T16)) → U12_ag(T89, T88, T15, T16, pF_in_agg(T89, T88, T15))
pF_in_agg(T89, T88, T15) → U5_agg(T89, T88, T15, lessD_in_ag(T89, T88))
lessD_in_ag(0, s(T99)) → lessD_out_ag(0, s(T99))
lessD_in_ag(s(T106), s(T105)) → U3_ag(T106, T105, lessD_in_ag(T106, T105))
U3_ag(T106, T105, lessD_out_ag(T106, T105)) → lessD_out_ag(s(T106), s(T105))
U5_agg(T89, T88, T15, lessD_out_ag(T89, T88)) → pF_out_agg(T89, T88, T15)
pF_in_agg(T92, T88, T15) → U6_agg(T92, T88, T15, lessD_in_ag(T92, T88))
U6_agg(T92, T88, T15, lessD_out_ag(T92, T88)) → U7_agg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T6, tree(T6, T7, T8)) → inG_out_gg(T6, tree(T6, T7, T8))
inG_in_gg(0, tree(s(T22), T15, T16)) → U11_gg(T22, T15, T16, inA_in_g(T15))
U11_gg(T22, T15, T16, inA_out_g(T15)) → inG_out_gg(0, tree(s(T22), T15, T16))
inG_in_gg(s(T89), tree(s(T88), T15, T16)) → U12_gg(T89, T88, T15, T16, pF_in_ggg(T89, T88, T15))
pF_in_ggg(T89, T88, T15) → U5_ggg(T89, T88, T15, lessD_in_gg(T89, T88))
lessD_in_gg(0, s(T99)) → lessD_out_gg(0, s(T99))
lessD_in_gg(s(T106), s(T105)) → U3_gg(T106, T105, lessD_in_gg(T106, T105))
U3_gg(T106, T105, lessD_out_gg(T106, T105)) → lessD_out_gg(s(T106), s(T105))
U5_ggg(T89, T88, T15, lessD_out_gg(T89, T88)) → pF_out_ggg(T89, T88, T15)
pF_in_ggg(T92, T88, T15) → U6_ggg(T92, T88, T15, lessD_in_gg(T92, T88))
U6_ggg(T92, T88, T15, lessD_out_gg(T92, T88)) → U7_ggg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T130, tree(T127, T128, T129)) → U13_gg(T130, T127, T128, T129, pH_in_ggg(T127, T130, T129))
pH_in_ggg(T127, T130, T129) → U8_ggg(T127, T130, T129, lessE_in_gg(T127, T130))
lessE_in_gg(0, s(T140)) → lessE_out_gg(0, s(T140))
lessE_in_gg(s(T145), s(T147)) → U4_gg(T145, T147, lessE_in_gg(T145, T147))
U4_gg(T145, T147, lessE_out_gg(T145, T147)) → lessE_out_gg(s(T145), s(T147))
U8_ggg(T127, T130, T129, lessE_out_gg(T127, T130)) → pH_out_ggg(T127, T130, T129)
pH_in_ggg(T127, T133, T129) → U9_ggg(T127, T133, T129, lessE_in_gg(T127, T133))
U9_ggg(T127, T133, T129, lessE_out_gg(T127, T133)) → U10_ggg(T127, T133, T129, inG_in_gg(T133, T129))
inG_in_gg(0, tree(s(T169), T162, T163)) → U14_gg(T169, T162, T163, inA_in_g(T162))
U14_gg(T169, T162, T163, inA_out_g(T162)) → inG_out_gg(0, tree(s(T169), T162, T163))
inG_in_gg(s(T184), tree(s(T183), T162, T163)) → U15_gg(T184, T183, T162, T163, pF_in_ggg(T184, T183, T162))
U15_gg(T184, T183, T162, T163, pF_out_ggg(T184, T183, T162)) → inG_out_gg(s(T184), tree(s(T183), T162, T163))
inG_in_gg(T202, tree(T199, T200, T201)) → U16_gg(T202, T199, T200, T201, pH_in_ggg(T199, T202, T201))
U16_gg(T202, T199, T200, T201, pH_out_ggg(T199, T202, T201)) → inG_out_gg(T202, tree(T199, T200, T201))
inG_in_gg(s(T219), tree(0, T211, T212)) → U17_gg(T219, T211, T212, inG_in_gg(s(T219), T212))
inG_in_gg(s(T232), tree(s(T230), T211, T212)) → U18_gg(T232, T230, T211, T212, lessE_in_gg(T230, T232))
U18_gg(T232, T230, T211, T212, lessE_out_gg(T230, T232)) → inG_out_gg(s(T232), tree(s(T230), T211, T212))
inG_in_gg(s(T235), tree(s(T230), T211, T212)) → U19_gg(T235, T230, T211, T212, lessE_in_gg(T230, T235))
U19_gg(T235, T230, T211, T212, lessE_out_gg(T230, T235)) → U20_gg(T235, T230, T211, T212, inG_in_gg(s(T235), T212))
U20_gg(T235, T230, T211, T212, inG_out_gg(s(T235), T212)) → inG_out_gg(s(T235), tree(s(T230), T211, T212))
U17_gg(T219, T211, T212, inG_out_gg(s(T219), T212)) → inG_out_gg(s(T219), tree(0, T211, T212))
U10_ggg(T127, T133, T129, inG_out_gg(T133, T129)) → pH_out_ggg(T127, T133, T129)
U13_gg(T130, T127, T128, T129, pH_out_ggg(T127, T130, T129)) → inG_out_gg(T130, tree(T127, T128, T129))
U7_ggg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_ggg(T92, T88, T15)
U12_gg(T89, T88, T15, T16, pF_out_ggg(T89, T88, T15)) → inG_out_gg(s(T89), tree(s(T88), T15, T16))
U7_agg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_agg(T92, T88, T15)
U12_ag(T89, T88, T15, T16, pF_out_agg(T89, T88, T15)) → inG_out_ag(s(T89), tree(s(T88), T15, T16))
inG_in_ag(T130, tree(T127, T128, T129)) → U13_ag(T130, T127, T128, T129, pH_in_gag(T127, T130, T129))
pH_in_gag(T127, T130, T129) → U8_gag(T127, T130, T129, lessE_in_ga(T127, T130))
lessE_in_ga(0, s(T140)) → lessE_out_ga(0, s(T140))
lessE_in_ga(s(T145), s(T147)) → U4_ga(T145, T147, lessE_in_ga(T145, T147))
U4_ga(T145, T147, lessE_out_ga(T145, T147)) → lessE_out_ga(s(T145), s(T147))
U8_gag(T127, T130, T129, lessE_out_ga(T127, T130)) → pH_out_gag(T127, T130, T129)
pH_in_gag(T127, T133, T129) → U9_gag(T127, T133, T129, lessE_in_ga(T127, T133))
U9_gag(T127, T133, T129, lessE_out_ga(T127, T133)) → U10_gag(T127, T133, T129, inG_in_ag(T133, T129))
inG_in_ag(0, tree(s(T169), T162, T163)) → U14_ag(T169, T162, T163, inA_in_g(T162))
U14_ag(T169, T162, T163, inA_out_g(T162)) → inG_out_ag(0, tree(s(T169), T162, T163))
inG_in_ag(s(T184), tree(s(T183), T162, T163)) → U15_ag(T184, T183, T162, T163, pF_in_agg(T184, T183, T162))
U15_ag(T184, T183, T162, T163, pF_out_agg(T184, T183, T162)) → inG_out_ag(s(T184), tree(s(T183), T162, T163))
inG_in_ag(T202, tree(T199, T200, T201)) → U16_ag(T202, T199, T200, T201, pH_in_gag(T199, T202, T201))
U16_ag(T202, T199, T200, T201, pH_out_gag(T199, T202, T201)) → inG_out_ag(T202, tree(T199, T200, T201))
inG_in_ag(s(T219), tree(0, T211, T212)) → U17_ag(T219, T211, T212, inG_in_ag(s(T219), T212))
inG_in_ag(s(T232), tree(s(T230), T211, T212)) → U18_ag(T232, T230, T211, T212, lessE_in_ga(T230, T232))
U18_ag(T232, T230, T211, T212, lessE_out_ga(T230, T232)) → inG_out_ag(s(T232), tree(s(T230), T211, T212))
inG_in_ag(s(T235), tree(s(T230), T211, T212)) → U19_ag(T235, T230, T211, T212, lessE_in_ga(T230, T235))
U19_ag(T235, T230, T211, T212, lessE_out_ga(T230, T235)) → U20_ag(T235, T230, T211, T212, inG_in_ag(s(T235), T212))
U20_ag(T235, T230, T211, T212, inG_out_ag(s(T235), T212)) → inG_out_ag(s(T235), tree(s(T230), T211, T212))
U17_ag(T219, T211, T212, inG_out_ag(s(T219), T212)) → inG_out_ag(s(T219), tree(0, T211, T212))
U10_gag(T127, T133, T129, inG_out_ag(T133, T129)) → pH_out_gag(T127, T133, T129)
U13_ag(T130, T127, T128, T129, pH_out_gag(T127, T130, T129)) → inG_out_ag(T130, tree(T127, T128, T129))
LESSD_IN_AG(s(T106), s(T105)) → LESSD_IN_AG(T106, T105)
LESSD_IN_AG(s(T105)) → LESSD_IN_AG(T105)
From the DPs we obtained the following set of size-change graphs:
U1_G(T49, T50, T51, lessB_out_g(T49)) → INA_IN_G(T50)
INA_IN_G(tree(T49, T50, T51)) → U1_G(T49, T50, T51, lessB_in_g(T49))
inG_in_ag(T6, tree(T6, T7, T8)) → inG_out_ag(T6, tree(T6, T7, T8))
inG_in_ag(0, tree(s(T22), T15, T16)) → U11_ag(T22, T15, T16, inA_in_g(T15))
inA_in_g(tree(0, T35, T36)) → inA_out_g(tree(0, T35, T36))
inA_in_g(tree(T49, T50, T51)) → U1_g(T49, T50, T51, lessB_in_g(T49))
lessB_in_g(s(T60)) → lessB_out_g(s(T60))
U1_g(T49, T50, T51, lessB_out_g(T49)) → inA_out_g(tree(T49, T50, T51))
U1_g(T49, T50, T51, lessB_out_g(T49)) → U2_g(T49, T50, T51, inA_in_g(T50))
U2_g(T49, T50, T51, inA_out_g(T50)) → inA_out_g(tree(T49, T50, T51))
U11_ag(T22, T15, T16, inA_out_g(T15)) → inG_out_ag(0, tree(s(T22), T15, T16))
inG_in_ag(s(T89), tree(s(T88), T15, T16)) → U12_ag(T89, T88, T15, T16, pF_in_agg(T89, T88, T15))
pF_in_agg(T89, T88, T15) → U5_agg(T89, T88, T15, lessD_in_ag(T89, T88))
lessD_in_ag(0, s(T99)) → lessD_out_ag(0, s(T99))
lessD_in_ag(s(T106), s(T105)) → U3_ag(T106, T105, lessD_in_ag(T106, T105))
U3_ag(T106, T105, lessD_out_ag(T106, T105)) → lessD_out_ag(s(T106), s(T105))
U5_agg(T89, T88, T15, lessD_out_ag(T89, T88)) → pF_out_agg(T89, T88, T15)
pF_in_agg(T92, T88, T15) → U6_agg(T92, T88, T15, lessD_in_ag(T92, T88))
U6_agg(T92, T88, T15, lessD_out_ag(T92, T88)) → U7_agg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T6, tree(T6, T7, T8)) → inG_out_gg(T6, tree(T6, T7, T8))
inG_in_gg(0, tree(s(T22), T15, T16)) → U11_gg(T22, T15, T16, inA_in_g(T15))
U11_gg(T22, T15, T16, inA_out_g(T15)) → inG_out_gg(0, tree(s(T22), T15, T16))
inG_in_gg(s(T89), tree(s(T88), T15, T16)) → U12_gg(T89, T88, T15, T16, pF_in_ggg(T89, T88, T15))
pF_in_ggg(T89, T88, T15) → U5_ggg(T89, T88, T15, lessD_in_gg(T89, T88))
lessD_in_gg(0, s(T99)) → lessD_out_gg(0, s(T99))
lessD_in_gg(s(T106), s(T105)) → U3_gg(T106, T105, lessD_in_gg(T106, T105))
U3_gg(T106, T105, lessD_out_gg(T106, T105)) → lessD_out_gg(s(T106), s(T105))
U5_ggg(T89, T88, T15, lessD_out_gg(T89, T88)) → pF_out_ggg(T89, T88, T15)
pF_in_ggg(T92, T88, T15) → U6_ggg(T92, T88, T15, lessD_in_gg(T92, T88))
U6_ggg(T92, T88, T15, lessD_out_gg(T92, T88)) → U7_ggg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T130, tree(T127, T128, T129)) → U13_gg(T130, T127, T128, T129, pH_in_ggg(T127, T130, T129))
pH_in_ggg(T127, T130, T129) → U8_ggg(T127, T130, T129, lessE_in_gg(T127, T130))
lessE_in_gg(0, s(T140)) → lessE_out_gg(0, s(T140))
lessE_in_gg(s(T145), s(T147)) → U4_gg(T145, T147, lessE_in_gg(T145, T147))
U4_gg(T145, T147, lessE_out_gg(T145, T147)) → lessE_out_gg(s(T145), s(T147))
U8_ggg(T127, T130, T129, lessE_out_gg(T127, T130)) → pH_out_ggg(T127, T130, T129)
pH_in_ggg(T127, T133, T129) → U9_ggg(T127, T133, T129, lessE_in_gg(T127, T133))
U9_ggg(T127, T133, T129, lessE_out_gg(T127, T133)) → U10_ggg(T127, T133, T129, inG_in_gg(T133, T129))
inG_in_gg(0, tree(s(T169), T162, T163)) → U14_gg(T169, T162, T163, inA_in_g(T162))
U14_gg(T169, T162, T163, inA_out_g(T162)) → inG_out_gg(0, tree(s(T169), T162, T163))
inG_in_gg(s(T184), tree(s(T183), T162, T163)) → U15_gg(T184, T183, T162, T163, pF_in_ggg(T184, T183, T162))
U15_gg(T184, T183, T162, T163, pF_out_ggg(T184, T183, T162)) → inG_out_gg(s(T184), tree(s(T183), T162, T163))
inG_in_gg(T202, tree(T199, T200, T201)) → U16_gg(T202, T199, T200, T201, pH_in_ggg(T199, T202, T201))
U16_gg(T202, T199, T200, T201, pH_out_ggg(T199, T202, T201)) → inG_out_gg(T202, tree(T199, T200, T201))
inG_in_gg(s(T219), tree(0, T211, T212)) → U17_gg(T219, T211, T212, inG_in_gg(s(T219), T212))
inG_in_gg(s(T232), tree(s(T230), T211, T212)) → U18_gg(T232, T230, T211, T212, lessE_in_gg(T230, T232))
U18_gg(T232, T230, T211, T212, lessE_out_gg(T230, T232)) → inG_out_gg(s(T232), tree(s(T230), T211, T212))
inG_in_gg(s(T235), tree(s(T230), T211, T212)) → U19_gg(T235, T230, T211, T212, lessE_in_gg(T230, T235))
U19_gg(T235, T230, T211, T212, lessE_out_gg(T230, T235)) → U20_gg(T235, T230, T211, T212, inG_in_gg(s(T235), T212))
U20_gg(T235, T230, T211, T212, inG_out_gg(s(T235), T212)) → inG_out_gg(s(T235), tree(s(T230), T211, T212))
U17_gg(T219, T211, T212, inG_out_gg(s(T219), T212)) → inG_out_gg(s(T219), tree(0, T211, T212))
U10_ggg(T127, T133, T129, inG_out_gg(T133, T129)) → pH_out_ggg(T127, T133, T129)
U13_gg(T130, T127, T128, T129, pH_out_ggg(T127, T130, T129)) → inG_out_gg(T130, tree(T127, T128, T129))
U7_ggg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_ggg(T92, T88, T15)
U12_gg(T89, T88, T15, T16, pF_out_ggg(T89, T88, T15)) → inG_out_gg(s(T89), tree(s(T88), T15, T16))
U7_agg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_agg(T92, T88, T15)
U12_ag(T89, T88, T15, T16, pF_out_agg(T89, T88, T15)) → inG_out_ag(s(T89), tree(s(T88), T15, T16))
inG_in_ag(T130, tree(T127, T128, T129)) → U13_ag(T130, T127, T128, T129, pH_in_gag(T127, T130, T129))
pH_in_gag(T127, T130, T129) → U8_gag(T127, T130, T129, lessE_in_ga(T127, T130))
lessE_in_ga(0, s(T140)) → lessE_out_ga(0, s(T140))
lessE_in_ga(s(T145), s(T147)) → U4_ga(T145, T147, lessE_in_ga(T145, T147))
U4_ga(T145, T147, lessE_out_ga(T145, T147)) → lessE_out_ga(s(T145), s(T147))
U8_gag(T127, T130, T129, lessE_out_ga(T127, T130)) → pH_out_gag(T127, T130, T129)
pH_in_gag(T127, T133, T129) → U9_gag(T127, T133, T129, lessE_in_ga(T127, T133))
U9_gag(T127, T133, T129, lessE_out_ga(T127, T133)) → U10_gag(T127, T133, T129, inG_in_ag(T133, T129))
inG_in_ag(0, tree(s(T169), T162, T163)) → U14_ag(T169, T162, T163, inA_in_g(T162))
U14_ag(T169, T162, T163, inA_out_g(T162)) → inG_out_ag(0, tree(s(T169), T162, T163))
inG_in_ag(s(T184), tree(s(T183), T162, T163)) → U15_ag(T184, T183, T162, T163, pF_in_agg(T184, T183, T162))
U15_ag(T184, T183, T162, T163, pF_out_agg(T184, T183, T162)) → inG_out_ag(s(T184), tree(s(T183), T162, T163))
inG_in_ag(T202, tree(T199, T200, T201)) → U16_ag(T202, T199, T200, T201, pH_in_gag(T199, T202, T201))
U16_ag(T202, T199, T200, T201, pH_out_gag(T199, T202, T201)) → inG_out_ag(T202, tree(T199, T200, T201))
inG_in_ag(s(T219), tree(0, T211, T212)) → U17_ag(T219, T211, T212, inG_in_ag(s(T219), T212))
inG_in_ag(s(T232), tree(s(T230), T211, T212)) → U18_ag(T232, T230, T211, T212, lessE_in_ga(T230, T232))
U18_ag(T232, T230, T211, T212, lessE_out_ga(T230, T232)) → inG_out_ag(s(T232), tree(s(T230), T211, T212))
inG_in_ag(s(T235), tree(s(T230), T211, T212)) → U19_ag(T235, T230, T211, T212, lessE_in_ga(T230, T235))
U19_ag(T235, T230, T211, T212, lessE_out_ga(T230, T235)) → U20_ag(T235, T230, T211, T212, inG_in_ag(s(T235), T212))
U20_ag(T235, T230, T211, T212, inG_out_ag(s(T235), T212)) → inG_out_ag(s(T235), tree(s(T230), T211, T212))
U17_ag(T219, T211, T212, inG_out_ag(s(T219), T212)) → inG_out_ag(s(T219), tree(0, T211, T212))
U10_gag(T127, T133, T129, inG_out_ag(T133, T129)) → pH_out_gag(T127, T133, T129)
U13_ag(T130, T127, T128, T129, pH_out_gag(T127, T130, T129)) → inG_out_ag(T130, tree(T127, T128, T129))
U1_G(T49, T50, T51, lessB_out_g(T49)) → INA_IN_G(T50)
INA_IN_G(tree(T49, T50, T51)) → U1_G(T49, T50, T51, lessB_in_g(T49))
lessB_in_g(s(T60)) → lessB_out_g(s(T60))
U1_G(T50, lessB_out_g) → INA_IN_G(T50)
INA_IN_G(tree(T49, T50, T51)) → U1_G(T50, lessB_in_g(T49))
lessB_in_g(s(T60)) → lessB_out_g
lessB_in_g(x0)
From the DPs we obtained the following set of size-change graphs:
ING_IN_GG(s(T89), tree(s(T88), T15, T16)) → PF_IN_GGG(T89, T88, T15)
PF_IN_GGG(T92, T88, T15) → U6_GGG(T92, T88, T15, lessD_in_gg(T92, T88))
U6_GGG(T92, T88, T15, lessD_out_gg(T92, T88)) → ING_IN_GG(s(T92), T15)
ING_IN_GG(T130, tree(T127, T128, T129)) → PH_IN_GGG(T127, T130, T129)
PH_IN_GGG(T127, T133, T129) → U9_GGG(T127, T133, T129, lessE_in_gg(T127, T133))
U9_GGG(T127, T133, T129, lessE_out_gg(T127, T133)) → ING_IN_GG(T133, T129)
ING_IN_GG(s(T219), tree(0, T211, T212)) → ING_IN_GG(s(T219), T212)
ING_IN_GG(s(T235), tree(s(T230), T211, T212)) → U19_GG(T235, T230, T211, T212, lessE_in_gg(T230, T235))
U19_GG(T235, T230, T211, T212, lessE_out_gg(T230, T235)) → ING_IN_GG(s(T235), T212)
inG_in_ag(T6, tree(T6, T7, T8)) → inG_out_ag(T6, tree(T6, T7, T8))
inG_in_ag(0, tree(s(T22), T15, T16)) → U11_ag(T22, T15, T16, inA_in_g(T15))
inA_in_g(tree(0, T35, T36)) → inA_out_g(tree(0, T35, T36))
inA_in_g(tree(T49, T50, T51)) → U1_g(T49, T50, T51, lessB_in_g(T49))
lessB_in_g(s(T60)) → lessB_out_g(s(T60))
U1_g(T49, T50, T51, lessB_out_g(T49)) → inA_out_g(tree(T49, T50, T51))
U1_g(T49, T50, T51, lessB_out_g(T49)) → U2_g(T49, T50, T51, inA_in_g(T50))
U2_g(T49, T50, T51, inA_out_g(T50)) → inA_out_g(tree(T49, T50, T51))
U11_ag(T22, T15, T16, inA_out_g(T15)) → inG_out_ag(0, tree(s(T22), T15, T16))
inG_in_ag(s(T89), tree(s(T88), T15, T16)) → U12_ag(T89, T88, T15, T16, pF_in_agg(T89, T88, T15))
pF_in_agg(T89, T88, T15) → U5_agg(T89, T88, T15, lessD_in_ag(T89, T88))
lessD_in_ag(0, s(T99)) → lessD_out_ag(0, s(T99))
lessD_in_ag(s(T106), s(T105)) → U3_ag(T106, T105, lessD_in_ag(T106, T105))
U3_ag(T106, T105, lessD_out_ag(T106, T105)) → lessD_out_ag(s(T106), s(T105))
U5_agg(T89, T88, T15, lessD_out_ag(T89, T88)) → pF_out_agg(T89, T88, T15)
pF_in_agg(T92, T88, T15) → U6_agg(T92, T88, T15, lessD_in_ag(T92, T88))
U6_agg(T92, T88, T15, lessD_out_ag(T92, T88)) → U7_agg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T6, tree(T6, T7, T8)) → inG_out_gg(T6, tree(T6, T7, T8))
inG_in_gg(0, tree(s(T22), T15, T16)) → U11_gg(T22, T15, T16, inA_in_g(T15))
U11_gg(T22, T15, T16, inA_out_g(T15)) → inG_out_gg(0, tree(s(T22), T15, T16))
inG_in_gg(s(T89), tree(s(T88), T15, T16)) → U12_gg(T89, T88, T15, T16, pF_in_ggg(T89, T88, T15))
pF_in_ggg(T89, T88, T15) → U5_ggg(T89, T88, T15, lessD_in_gg(T89, T88))
lessD_in_gg(0, s(T99)) → lessD_out_gg(0, s(T99))
lessD_in_gg(s(T106), s(T105)) → U3_gg(T106, T105, lessD_in_gg(T106, T105))
U3_gg(T106, T105, lessD_out_gg(T106, T105)) → lessD_out_gg(s(T106), s(T105))
U5_ggg(T89, T88, T15, lessD_out_gg(T89, T88)) → pF_out_ggg(T89, T88, T15)
pF_in_ggg(T92, T88, T15) → U6_ggg(T92, T88, T15, lessD_in_gg(T92, T88))
U6_ggg(T92, T88, T15, lessD_out_gg(T92, T88)) → U7_ggg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T130, tree(T127, T128, T129)) → U13_gg(T130, T127, T128, T129, pH_in_ggg(T127, T130, T129))
pH_in_ggg(T127, T130, T129) → U8_ggg(T127, T130, T129, lessE_in_gg(T127, T130))
lessE_in_gg(0, s(T140)) → lessE_out_gg(0, s(T140))
lessE_in_gg(s(T145), s(T147)) → U4_gg(T145, T147, lessE_in_gg(T145, T147))
U4_gg(T145, T147, lessE_out_gg(T145, T147)) → lessE_out_gg(s(T145), s(T147))
U8_ggg(T127, T130, T129, lessE_out_gg(T127, T130)) → pH_out_ggg(T127, T130, T129)
pH_in_ggg(T127, T133, T129) → U9_ggg(T127, T133, T129, lessE_in_gg(T127, T133))
U9_ggg(T127, T133, T129, lessE_out_gg(T127, T133)) → U10_ggg(T127, T133, T129, inG_in_gg(T133, T129))
inG_in_gg(0, tree(s(T169), T162, T163)) → U14_gg(T169, T162, T163, inA_in_g(T162))
U14_gg(T169, T162, T163, inA_out_g(T162)) → inG_out_gg(0, tree(s(T169), T162, T163))
inG_in_gg(s(T184), tree(s(T183), T162, T163)) → U15_gg(T184, T183, T162, T163, pF_in_ggg(T184, T183, T162))
U15_gg(T184, T183, T162, T163, pF_out_ggg(T184, T183, T162)) → inG_out_gg(s(T184), tree(s(T183), T162, T163))
inG_in_gg(T202, tree(T199, T200, T201)) → U16_gg(T202, T199, T200, T201, pH_in_ggg(T199, T202, T201))
U16_gg(T202, T199, T200, T201, pH_out_ggg(T199, T202, T201)) → inG_out_gg(T202, tree(T199, T200, T201))
inG_in_gg(s(T219), tree(0, T211, T212)) → U17_gg(T219, T211, T212, inG_in_gg(s(T219), T212))
inG_in_gg(s(T232), tree(s(T230), T211, T212)) → U18_gg(T232, T230, T211, T212, lessE_in_gg(T230, T232))
U18_gg(T232, T230, T211, T212, lessE_out_gg(T230, T232)) → inG_out_gg(s(T232), tree(s(T230), T211, T212))
inG_in_gg(s(T235), tree(s(T230), T211, T212)) → U19_gg(T235, T230, T211, T212, lessE_in_gg(T230, T235))
U19_gg(T235, T230, T211, T212, lessE_out_gg(T230, T235)) → U20_gg(T235, T230, T211, T212, inG_in_gg(s(T235), T212))
U20_gg(T235, T230, T211, T212, inG_out_gg(s(T235), T212)) → inG_out_gg(s(T235), tree(s(T230), T211, T212))
U17_gg(T219, T211, T212, inG_out_gg(s(T219), T212)) → inG_out_gg(s(T219), tree(0, T211, T212))
U10_ggg(T127, T133, T129, inG_out_gg(T133, T129)) → pH_out_ggg(T127, T133, T129)
U13_gg(T130, T127, T128, T129, pH_out_ggg(T127, T130, T129)) → inG_out_gg(T130, tree(T127, T128, T129))
U7_ggg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_ggg(T92, T88, T15)
U12_gg(T89, T88, T15, T16, pF_out_ggg(T89, T88, T15)) → inG_out_gg(s(T89), tree(s(T88), T15, T16))
U7_agg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_agg(T92, T88, T15)
U12_ag(T89, T88, T15, T16, pF_out_agg(T89, T88, T15)) → inG_out_ag(s(T89), tree(s(T88), T15, T16))
inG_in_ag(T130, tree(T127, T128, T129)) → U13_ag(T130, T127, T128, T129, pH_in_gag(T127, T130, T129))
pH_in_gag(T127, T130, T129) → U8_gag(T127, T130, T129, lessE_in_ga(T127, T130))
lessE_in_ga(0, s(T140)) → lessE_out_ga(0, s(T140))
lessE_in_ga(s(T145), s(T147)) → U4_ga(T145, T147, lessE_in_ga(T145, T147))
U4_ga(T145, T147, lessE_out_ga(T145, T147)) → lessE_out_ga(s(T145), s(T147))
U8_gag(T127, T130, T129, lessE_out_ga(T127, T130)) → pH_out_gag(T127, T130, T129)
pH_in_gag(T127, T133, T129) → U9_gag(T127, T133, T129, lessE_in_ga(T127, T133))
U9_gag(T127, T133, T129, lessE_out_ga(T127, T133)) → U10_gag(T127, T133, T129, inG_in_ag(T133, T129))
inG_in_ag(0, tree(s(T169), T162, T163)) → U14_ag(T169, T162, T163, inA_in_g(T162))
U14_ag(T169, T162, T163, inA_out_g(T162)) → inG_out_ag(0, tree(s(T169), T162, T163))
inG_in_ag(s(T184), tree(s(T183), T162, T163)) → U15_ag(T184, T183, T162, T163, pF_in_agg(T184, T183, T162))
U15_ag(T184, T183, T162, T163, pF_out_agg(T184, T183, T162)) → inG_out_ag(s(T184), tree(s(T183), T162, T163))
inG_in_ag(T202, tree(T199, T200, T201)) → U16_ag(T202, T199, T200, T201, pH_in_gag(T199, T202, T201))
U16_ag(T202, T199, T200, T201, pH_out_gag(T199, T202, T201)) → inG_out_ag(T202, tree(T199, T200, T201))
inG_in_ag(s(T219), tree(0, T211, T212)) → U17_ag(T219, T211, T212, inG_in_ag(s(T219), T212))
inG_in_ag(s(T232), tree(s(T230), T211, T212)) → U18_ag(T232, T230, T211, T212, lessE_in_ga(T230, T232))
U18_ag(T232, T230, T211, T212, lessE_out_ga(T230, T232)) → inG_out_ag(s(T232), tree(s(T230), T211, T212))
inG_in_ag(s(T235), tree(s(T230), T211, T212)) → U19_ag(T235, T230, T211, T212, lessE_in_ga(T230, T235))
U19_ag(T235, T230, T211, T212, lessE_out_ga(T230, T235)) → U20_ag(T235, T230, T211, T212, inG_in_ag(s(T235), T212))
U20_ag(T235, T230, T211, T212, inG_out_ag(s(T235), T212)) → inG_out_ag(s(T235), tree(s(T230), T211, T212))
U17_ag(T219, T211, T212, inG_out_ag(s(T219), T212)) → inG_out_ag(s(T219), tree(0, T211, T212))
U10_gag(T127, T133, T129, inG_out_ag(T133, T129)) → pH_out_gag(T127, T133, T129)
U13_ag(T130, T127, T128, T129, pH_out_gag(T127, T130, T129)) → inG_out_ag(T130, tree(T127, T128, T129))
ING_IN_GG(s(T89), tree(s(T88), T15, T16)) → PF_IN_GGG(T89, T88, T15)
PF_IN_GGG(T92, T88, T15) → U6_GGG(T92, T88, T15, lessD_in_gg(T92, T88))
U6_GGG(T92, T88, T15, lessD_out_gg(T92, T88)) → ING_IN_GG(s(T92), T15)
ING_IN_GG(T130, tree(T127, T128, T129)) → PH_IN_GGG(T127, T130, T129)
PH_IN_GGG(T127, T133, T129) → U9_GGG(T127, T133, T129, lessE_in_gg(T127, T133))
U9_GGG(T127, T133, T129, lessE_out_gg(T127, T133)) → ING_IN_GG(T133, T129)
ING_IN_GG(s(T219), tree(0, T211, T212)) → ING_IN_GG(s(T219), T212)
ING_IN_GG(s(T235), tree(s(T230), T211, T212)) → U19_GG(T235, T230, T211, T212, lessE_in_gg(T230, T235))
U19_GG(T235, T230, T211, T212, lessE_out_gg(T230, T235)) → ING_IN_GG(s(T235), T212)
lessD_in_gg(0, s(T99)) → lessD_out_gg(0, s(T99))
lessD_in_gg(s(T106), s(T105)) → U3_gg(T106, T105, lessD_in_gg(T106, T105))
lessE_in_gg(0, s(T140)) → lessE_out_gg(0, s(T140))
lessE_in_gg(s(T145), s(T147)) → U4_gg(T145, T147, lessE_in_gg(T145, T147))
U3_gg(T106, T105, lessD_out_gg(T106, T105)) → lessD_out_gg(s(T106), s(T105))
U4_gg(T145, T147, lessE_out_gg(T145, T147)) → lessE_out_gg(s(T145), s(T147))
ING_IN_GG(s(T89), tree(s(T88), T15, T16)) → PF_IN_GGG(T89, T88, T15)
PF_IN_GGG(T92, T88, T15) → U6_GGG(T92, T15, lessD_in_gg(T92, T88))
U6_GGG(T92, T15, lessD_out_gg) → ING_IN_GG(s(T92), T15)
ING_IN_GG(T130, tree(T127, T128, T129)) → PH_IN_GGG(T127, T130, T129)
PH_IN_GGG(T127, T133, T129) → U9_GGG(T133, T129, lessE_in_gg(T127, T133))
U9_GGG(T133, T129, lessE_out_gg) → ING_IN_GG(T133, T129)
ING_IN_GG(s(T219), tree(0, T211, T212)) → ING_IN_GG(s(T219), T212)
ING_IN_GG(s(T235), tree(s(T230), T211, T212)) → U19_GG(T235, T212, lessE_in_gg(T230, T235))
U19_GG(T235, T212, lessE_out_gg) → ING_IN_GG(s(T235), T212)
lessD_in_gg(0, s(T99)) → lessD_out_gg
lessD_in_gg(s(T106), s(T105)) → U3_gg(lessD_in_gg(T106, T105))
lessE_in_gg(0, s(T140)) → lessE_out_gg
lessE_in_gg(s(T145), s(T147)) → U4_gg(lessE_in_gg(T145, T147))
U3_gg(lessD_out_gg) → lessD_out_gg
U4_gg(lessE_out_gg) → lessE_out_gg
lessD_in_gg(x0, x1)
lessE_in_gg(x0, x1)
U3_gg(x0)
U4_gg(x0)
From the DPs we obtained the following set of size-change graphs:
ING_IN_AG(T130, tree(T127, T128, T129)) → PH_IN_GAG(T127, T130, T129)
PH_IN_GAG(T127, T133, T129) → U9_GAG(T127, T133, T129, lessE_in_ga(T127, T133))
U9_GAG(T127, T133, T129, lessE_out_ga(T127, T133)) → ING_IN_AG(T133, T129)
ING_IN_AG(s(T219), tree(0, T211, T212)) → ING_IN_AG(s(T219), T212)
ING_IN_AG(s(T235), tree(s(T230), T211, T212)) → U19_AG(T235, T230, T211, T212, lessE_in_ga(T230, T235))
U19_AG(T235, T230, T211, T212, lessE_out_ga(T230, T235)) → ING_IN_AG(s(T235), T212)
inG_in_ag(T6, tree(T6, T7, T8)) → inG_out_ag(T6, tree(T6, T7, T8))
inG_in_ag(0, tree(s(T22), T15, T16)) → U11_ag(T22, T15, T16, inA_in_g(T15))
inA_in_g(tree(0, T35, T36)) → inA_out_g(tree(0, T35, T36))
inA_in_g(tree(T49, T50, T51)) → U1_g(T49, T50, T51, lessB_in_g(T49))
lessB_in_g(s(T60)) → lessB_out_g(s(T60))
U1_g(T49, T50, T51, lessB_out_g(T49)) → inA_out_g(tree(T49, T50, T51))
U1_g(T49, T50, T51, lessB_out_g(T49)) → U2_g(T49, T50, T51, inA_in_g(T50))
U2_g(T49, T50, T51, inA_out_g(T50)) → inA_out_g(tree(T49, T50, T51))
U11_ag(T22, T15, T16, inA_out_g(T15)) → inG_out_ag(0, tree(s(T22), T15, T16))
inG_in_ag(s(T89), tree(s(T88), T15, T16)) → U12_ag(T89, T88, T15, T16, pF_in_agg(T89, T88, T15))
pF_in_agg(T89, T88, T15) → U5_agg(T89, T88, T15, lessD_in_ag(T89, T88))
lessD_in_ag(0, s(T99)) → lessD_out_ag(0, s(T99))
lessD_in_ag(s(T106), s(T105)) → U3_ag(T106, T105, lessD_in_ag(T106, T105))
U3_ag(T106, T105, lessD_out_ag(T106, T105)) → lessD_out_ag(s(T106), s(T105))
U5_agg(T89, T88, T15, lessD_out_ag(T89, T88)) → pF_out_agg(T89, T88, T15)
pF_in_agg(T92, T88, T15) → U6_agg(T92, T88, T15, lessD_in_ag(T92, T88))
U6_agg(T92, T88, T15, lessD_out_ag(T92, T88)) → U7_agg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T6, tree(T6, T7, T8)) → inG_out_gg(T6, tree(T6, T7, T8))
inG_in_gg(0, tree(s(T22), T15, T16)) → U11_gg(T22, T15, T16, inA_in_g(T15))
U11_gg(T22, T15, T16, inA_out_g(T15)) → inG_out_gg(0, tree(s(T22), T15, T16))
inG_in_gg(s(T89), tree(s(T88), T15, T16)) → U12_gg(T89, T88, T15, T16, pF_in_ggg(T89, T88, T15))
pF_in_ggg(T89, T88, T15) → U5_ggg(T89, T88, T15, lessD_in_gg(T89, T88))
lessD_in_gg(0, s(T99)) → lessD_out_gg(0, s(T99))
lessD_in_gg(s(T106), s(T105)) → U3_gg(T106, T105, lessD_in_gg(T106, T105))
U3_gg(T106, T105, lessD_out_gg(T106, T105)) → lessD_out_gg(s(T106), s(T105))
U5_ggg(T89, T88, T15, lessD_out_gg(T89, T88)) → pF_out_ggg(T89, T88, T15)
pF_in_ggg(T92, T88, T15) → U6_ggg(T92, T88, T15, lessD_in_gg(T92, T88))
U6_ggg(T92, T88, T15, lessD_out_gg(T92, T88)) → U7_ggg(T92, T88, T15, inG_in_gg(s(T92), T15))
inG_in_gg(T130, tree(T127, T128, T129)) → U13_gg(T130, T127, T128, T129, pH_in_ggg(T127, T130, T129))
pH_in_ggg(T127, T130, T129) → U8_ggg(T127, T130, T129, lessE_in_gg(T127, T130))
lessE_in_gg(0, s(T140)) → lessE_out_gg(0, s(T140))
lessE_in_gg(s(T145), s(T147)) → U4_gg(T145, T147, lessE_in_gg(T145, T147))
U4_gg(T145, T147, lessE_out_gg(T145, T147)) → lessE_out_gg(s(T145), s(T147))
U8_ggg(T127, T130, T129, lessE_out_gg(T127, T130)) → pH_out_ggg(T127, T130, T129)
pH_in_ggg(T127, T133, T129) → U9_ggg(T127, T133, T129, lessE_in_gg(T127, T133))
U9_ggg(T127, T133, T129, lessE_out_gg(T127, T133)) → U10_ggg(T127, T133, T129, inG_in_gg(T133, T129))
inG_in_gg(0, tree(s(T169), T162, T163)) → U14_gg(T169, T162, T163, inA_in_g(T162))
U14_gg(T169, T162, T163, inA_out_g(T162)) → inG_out_gg(0, tree(s(T169), T162, T163))
inG_in_gg(s(T184), tree(s(T183), T162, T163)) → U15_gg(T184, T183, T162, T163, pF_in_ggg(T184, T183, T162))
U15_gg(T184, T183, T162, T163, pF_out_ggg(T184, T183, T162)) → inG_out_gg(s(T184), tree(s(T183), T162, T163))
inG_in_gg(T202, tree(T199, T200, T201)) → U16_gg(T202, T199, T200, T201, pH_in_ggg(T199, T202, T201))
U16_gg(T202, T199, T200, T201, pH_out_ggg(T199, T202, T201)) → inG_out_gg(T202, tree(T199, T200, T201))
inG_in_gg(s(T219), tree(0, T211, T212)) → U17_gg(T219, T211, T212, inG_in_gg(s(T219), T212))
inG_in_gg(s(T232), tree(s(T230), T211, T212)) → U18_gg(T232, T230, T211, T212, lessE_in_gg(T230, T232))
U18_gg(T232, T230, T211, T212, lessE_out_gg(T230, T232)) → inG_out_gg(s(T232), tree(s(T230), T211, T212))
inG_in_gg(s(T235), tree(s(T230), T211, T212)) → U19_gg(T235, T230, T211, T212, lessE_in_gg(T230, T235))
U19_gg(T235, T230, T211, T212, lessE_out_gg(T230, T235)) → U20_gg(T235, T230, T211, T212, inG_in_gg(s(T235), T212))
U20_gg(T235, T230, T211, T212, inG_out_gg(s(T235), T212)) → inG_out_gg(s(T235), tree(s(T230), T211, T212))
U17_gg(T219, T211, T212, inG_out_gg(s(T219), T212)) → inG_out_gg(s(T219), tree(0, T211, T212))
U10_ggg(T127, T133, T129, inG_out_gg(T133, T129)) → pH_out_ggg(T127, T133, T129)
U13_gg(T130, T127, T128, T129, pH_out_ggg(T127, T130, T129)) → inG_out_gg(T130, tree(T127, T128, T129))
U7_ggg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_ggg(T92, T88, T15)
U12_gg(T89, T88, T15, T16, pF_out_ggg(T89, T88, T15)) → inG_out_gg(s(T89), tree(s(T88), T15, T16))
U7_agg(T92, T88, T15, inG_out_gg(s(T92), T15)) → pF_out_agg(T92, T88, T15)
U12_ag(T89, T88, T15, T16, pF_out_agg(T89, T88, T15)) → inG_out_ag(s(T89), tree(s(T88), T15, T16))
inG_in_ag(T130, tree(T127, T128, T129)) → U13_ag(T130, T127, T128, T129, pH_in_gag(T127, T130, T129))
pH_in_gag(T127, T130, T129) → U8_gag(T127, T130, T129, lessE_in_ga(T127, T130))
lessE_in_ga(0, s(T140)) → lessE_out_ga(0, s(T140))
lessE_in_ga(s(T145), s(T147)) → U4_ga(T145, T147, lessE_in_ga(T145, T147))
U4_ga(T145, T147, lessE_out_ga(T145, T147)) → lessE_out_ga(s(T145), s(T147))
U8_gag(T127, T130, T129, lessE_out_ga(T127, T130)) → pH_out_gag(T127, T130, T129)
pH_in_gag(T127, T133, T129) → U9_gag(T127, T133, T129, lessE_in_ga(T127, T133))
U9_gag(T127, T133, T129, lessE_out_ga(T127, T133)) → U10_gag(T127, T133, T129, inG_in_ag(T133, T129))
inG_in_ag(0, tree(s(T169), T162, T163)) → U14_ag(T169, T162, T163, inA_in_g(T162))
U14_ag(T169, T162, T163, inA_out_g(T162)) → inG_out_ag(0, tree(s(T169), T162, T163))
inG_in_ag(s(T184), tree(s(T183), T162, T163)) → U15_ag(T184, T183, T162, T163, pF_in_agg(T184, T183, T162))
U15_ag(T184, T183, T162, T163, pF_out_agg(T184, T183, T162)) → inG_out_ag(s(T184), tree(s(T183), T162, T163))
inG_in_ag(T202, tree(T199, T200, T201)) → U16_ag(T202, T199, T200, T201, pH_in_gag(T199, T202, T201))
U16_ag(T202, T199, T200, T201, pH_out_gag(T199, T202, T201)) → inG_out_ag(T202, tree(T199, T200, T201))
inG_in_ag(s(T219), tree(0, T211, T212)) → U17_ag(T219, T211, T212, inG_in_ag(s(T219), T212))
inG_in_ag(s(T232), tree(s(T230), T211, T212)) → U18_ag(T232, T230, T211, T212, lessE_in_ga(T230, T232))
U18_ag(T232, T230, T211, T212, lessE_out_ga(T230, T232)) → inG_out_ag(s(T232), tree(s(T230), T211, T212))
inG_in_ag(s(T235), tree(s(T230), T211, T212)) → U19_ag(T235, T230, T211, T212, lessE_in_ga(T230, T235))
U19_ag(T235, T230, T211, T212, lessE_out_ga(T230, T235)) → U20_ag(T235, T230, T211, T212, inG_in_ag(s(T235), T212))
U20_ag(T235, T230, T211, T212, inG_out_ag(s(T235), T212)) → inG_out_ag(s(T235), tree(s(T230), T211, T212))
U17_ag(T219, T211, T212, inG_out_ag(s(T219), T212)) → inG_out_ag(s(T219), tree(0, T211, T212))
U10_gag(T127, T133, T129, inG_out_ag(T133, T129)) → pH_out_gag(T127, T133, T129)
U13_ag(T130, T127, T128, T129, pH_out_gag(T127, T130, T129)) → inG_out_ag(T130, tree(T127, T128, T129))
ING_IN_AG(T130, tree(T127, T128, T129)) → PH_IN_GAG(T127, T130, T129)
PH_IN_GAG(T127, T133, T129) → U9_GAG(T127, T133, T129, lessE_in_ga(T127, T133))
U9_GAG(T127, T133, T129, lessE_out_ga(T127, T133)) → ING_IN_AG(T133, T129)
ING_IN_AG(s(T219), tree(0, T211, T212)) → ING_IN_AG(s(T219), T212)
ING_IN_AG(s(T235), tree(s(T230), T211, T212)) → U19_AG(T235, T230, T211, T212, lessE_in_ga(T230, T235))
U19_AG(T235, T230, T211, T212, lessE_out_ga(T230, T235)) → ING_IN_AG(s(T235), T212)
lessE_in_ga(0, s(T140)) → lessE_out_ga(0, s(T140))
lessE_in_ga(s(T145), s(T147)) → U4_ga(T145, T147, lessE_in_ga(T145, T147))
U4_ga(T145, T147, lessE_out_ga(T145, T147)) → lessE_out_ga(s(T145), s(T147))
ING_IN_AG(tree(T127, T128, T129)) → PH_IN_GAG(T127, T129)
PH_IN_GAG(T127, T129) → U9_GAG(T129, lessE_in_ga(T127))
U9_GAG(T129, lessE_out_ga) → ING_IN_AG(T129)
ING_IN_AG(tree(0, T211, T212)) → ING_IN_AG(T212)
ING_IN_AG(tree(s(T230), T211, T212)) → U19_AG(T212, lessE_in_ga(T230))
U19_AG(T212, lessE_out_ga) → ING_IN_AG(T212)
lessE_in_ga(0) → lessE_out_ga
lessE_in_ga(s(T145)) → U4_ga(lessE_in_ga(T145))
U4_ga(lessE_out_ga) → lessE_out_ga
lessE_in_ga(x0)
U4_ga(x0)
From the DPs we obtained the following set of size-change graphs: